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.
Hope this helps,
On 10/08/17 14:22, Peter Gammie wrote:
Dear BNF experts,
The `size` function for `fmap` in HOL/Library/Finite_Map in Isabelle2016-1 seems sub-optimal: it appears to ignore the sizes of the things in the map.
I tried implementing this using the approach taken in FSet and Multiset, but the `fmap` constructor is binary and Iâm not sure what shape the theorems should be (specifically the final one that composes size functions somehow).
This archive was generated by a fusion of
Pipermail (Mailman edition) and