Is there a simple way to fix a type variable in a context such that all appearances of this variable have the same sort? I would expect something like the following where
some_sort could be a type class:
context fixes 'a::some_sort begin ... end
The only way to achieve this that I know of would be a dummy locale like
locale dummy_locale = fixes dummy :: "'a::some_sort".
Behold my arcane Isabelle magic!
context assumes "SORT_CONSTRAINT('a :: some_sort)" begin … end
This is actually less arcane than I expected. Thanks a lot.
Florian Sextl has marked this topic as resolved.
Last updated: Dec 07 2023 at 08:19 UTC