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



> Thanks for the pointers. I donât recall seeing the stuff you mentioned about [measure_function] being mentioned in the `functions` manual; perhaps it could be added?

Possibly. Though I'll have to defer to someone who actually understands
the implications of declaring [measure_functions], in particular the
parametrized variants.

Cheers
Lars





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