Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)
> You need a function size_fmap that takes a size function for every type
> argument, even the dead ones. So it should have the type
> ('a => nat) => ('b => nat) => ('a, 'b) fmap => nat
> Typically, the instantiation for the type class then puts "%_. 0" for
> the arguments.
This is an oversight â I'll try to add this to the theory over the next
couple of days.
This archive was generated by a fusion of
Pipermail (Mailman edition) and