[isabelle] size setup for HOL/Library/Finite_Map (fmap)
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