Stream: General

Topic: ✔ Fixed type variable


view this post on Zulip 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".

view this post on Zulip Manuel Eberl (Dec 08 2021 at 16:12):

Behold my arcane Isabelle magic!

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

end

view this post on Zulip Florian Sextl (Dec 08 2021 at 16:14):

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

view this post on Zulip Notification Bot (Dec 08 2021 at 16:14):

Florian Sextl has marked this topic as resolved.


Last updated: Aug 15 2022 at 02:13 UTC