Re: [isabelle] Usability of lift_bnf/copy_bnf



Dear Lars,

> This is as expected. However, I noticed some problems when working with
> these constants wrt to other Isabelle tools and the BNF package itself:

I will let Dmitriy and/or handle most of your questions, since they're in charge of these parts. But here's some immediate help regarding one of them.

> * The defining equations are not exported. I had to obtain them via
> [...]
> 
> * I can't give them a custom name. If I want to rename 'map_fmap' to
> 'fmmap', I need to explicitly add an abbreviation.

The "them" in the second point presumably refers to the constants introduced by the command, esp. the map function and the relator.

In this case, I'm not sure where you get this notion from. If you look at "isabelle doc datatypes", you will find a syntactic item called map-rel in the syntax of "lift_bnf" and "copy_bnf". You can use that to specify custom names to the map function and the relator, e.g.

     lift_bnf ('a, 'b) fmap [wits: Map.empty] for map: fmmap
       by auto

I hope this helps.

Jasmin





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