Re: [isabelle] find_consts does not find constants from BNF package



Hi Andreas,

thanks for the report. (The BNF constants were concealed for almost two years now, without anyone noticing!)

It should be better with the repository version isabelle/69a97fc33f7a.

Dmitriy

On 22.09.2015 17:07, Andreas Lochbihler wrote:
Dear BNF developers,

I noticed that find_consts does not find the constants for the set and map functions and the relator. For _ list, for example, none of the following commands find the functions defined by the datatype declaration in List.thy (in Isabelle2015):

find_consts "(_ â _) â _ list â _ list" (* map not found *)
find_consts "(_ â _ â bool) â _ list â _ list â bool" (* list_all2 not found *)
find_consts "_ list â _ set" (* set not found *)

Could this be changed such that find_consts can find them? I was puzzled today in our Isabelle course when I wanted to search for map and find_consts simply did not show it.

Best,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.