Alex Mobius (Feb 24 2026 at 17:13): Alex Mobius (Feb 24 2026 at 17:13):I've been using HOL-Library.Finite_Map in my theories and have noticed a couple of warts:
map_restrict_set is Map.restrict_map with arguments swapped, set_of_map is Map.graph. The corresponding fmap_restrict also doesn't have any syntax to it. The common definitions have more lemmas that could be transferred, but I don't know how much value there is in making the aliases explicit.fmap_subseteq is missing partial order lemmas (unsure if order instantiation is warranted here - it exists for unbounded maps). These partial lemmas are trivial to prove by transfer', but surprisingly tricky using just the provided lemmas (even reflexivity is non-trivial!) - they should IMO definitely be included. Fabian Huch (Feb 24 2026 at 17:19):Alex Mobius said:
I'm happy to contribute on these counts, but don't really know what the model for that is - I hope I don't need a scholarship at TUM :).
The model is to propose the changes in question on the users mailing list.
Alex Mobius (Feb 24 2026 at 19:43):@Fabian Huch thank you. How do I format them, as hg patches or is it better to start with a textual proposition?
Kevin Kappelmann (Feb 24 2026 at 20:56):I brief summary and a patch file should be fine.
Last updated: Feb 27 2026 at 20:31 UTC