Stream: General

Topic: ✔ Fixed type variable

Florian Sextl (Dec 08 2021 at 15:59):

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".

Manuel Eberl (Dec 08 2021 at 16:12):

Behold my arcane Isabelle magic!

context
assumes "SORT_CONSTRAINT('a :: some_sort)"
begin
…
end

Florian Sextl (Dec 08 2021 at 16:14):

This is actually less arcane than I expected. Thanks a lot.

Notification Bot (Dec 08 2021 at 16:14):

Florian Sextl has marked this topic as resolved.

Last updated: Apr 20 2024 at 08:16 UTC