Re: [isabelle] Usability of lift_bnf/copy_bnf
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and