Email Gateway (May 06 2026 at 14:39): Email Gateway (May 06 2026 at 14:39):From: Alex Mobius <cl-isabelle-users@lists.cam.ac.uk>
Hello, trying to figure out why theorems of classes po, cpo are imported into "bifinite" context in a broken form (as if they're coming from a corresponding locale, not from a superclass).
See attachment for minimal reproduction I've achieved. From what I can understand, this happens because the additional assumption on class bifinite uses a definition with constrains a sort on type variable 'a. I am able to create my own class reproducing the issue, and the issue is also observed in "context bifinite". Weirdly, with HOL typeclasses the definition is rejected altogether if the superclass in class declaration is stricter than the sort constraint.
This all seems to be a collection of weird edge cases, and I'm not sure what to make of it. I know HOLCF isn't very popular, and haven't found any luck on Zulip so far. Maybe I'm lucky, and a knowledgeable person will help me suss it out?
I am using Isabelle 2025-2.
--
With utmost respect,
Alex.
Last updated: May 23 2026 at 03:31 UTC