Re: [isabelle] Usability of lift_bnf/copy_bnf



Hi Jasmin,

> 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 stand corrected. I thought I tried that syntax and it didn't work, but
I must have done something wrong. It works now.

Cheers
Lars




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