Stream: Beginner Questions

Topic: Sort inference?


view this post on Zulip Ian Blumenfeld (Apr 23 2021 at 12:05):

If I want to define some super using:

type_synonym 'a double_word = 'a bit0 word

It seems whenever I want to use 'a double_word as a type in a function or lemma, I need to specify ('a::len0)

Is there some way around this just to improve readability?

view this post on Zulip Mathias Fleury (Apr 23 2021 at 13:18):

No (see https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00106.html)

view this post on Zulip Manuel Eberl (Apr 23 2021 at 13:21):

There is one thing you can do:

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

end

Inside that context, the type variable 'a will always have a len0 attached to it. Note however that the 'a is fixed in this entire context. That means that if you prove some theorem involving 'a, you will not be able to use it for any other type before you leave the context (i.e. the implicit polymorphism only comes into effect once you leave the context).

view this post on Zulip Manuel Eberl (Apr 23 2021 at 13:22):

Just one of those little-known Isabelle hacks that I saw somewhere once and thought ‘Wow, this is terrible. I will start using it immediately!’


Last updated: Aug 13 2022 at 04:29 UTC