Re: [isabelle] Usability of lift_bnf/copy_bnf

Hi Dmitriy,

> 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
> happens.

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:

lemma fmmap_lifting[transfer_rule]:
  "(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 MHonArc.