Re: [isabelle] size setup for HOL/Library/Finite_Map (fmap)



On 11 Aug 2017, at 05:41, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> 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.

Great, thanks!

cheers,
peter



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