Re: [isabelle] Usability of lift_bnf/copy_bnf
> I think your way of dealing with those limitations (they also apply
> to set and rel) are as good as it can get for now. They are on my
> list of things to improve. Eventually, Iâll report here when this
glad to hear that you're on it :-)
For posterity, here's an improved version of getting transfer to work,
as pointed out by Johannes:
"(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =)
(Îf. op â (map_option f)) fmmap"
The proof is a little bit more complicated, but this avoids introducing
an extraneous constant.
This archive was generated by a fusion of
Pipermail (Mailman edition) and