Email Gateway (May 22 2026 at 15:14): Email Gateway (May 22 2026 at 15:14):From: Alex Mobius <cl-isabelle-users@lists.cam.ac.uk>
Good day,
I was told this is an appropriate place to propose contributions to the standard library. I noticed that the "extended" arity in HOL-Library is missing the complete_lattice and complete_linear_order instances (they are present more specifically for enat and ereal). Seems like an obvious and useful thing to have, so I thought I'd share the implementation I came up with - maybe value is found in including some form of it into HOL-Library.
Best regards,
Alex.
Last updated: May 23 2026 at 03:31 UTC