Ian Blumenfeld (Apr 23 2021 at 12:05): 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?
Mathias Fleury (Apr 23 2021 at 13:18):No (see https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00106.html)
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).
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: Apr 24 2024 at 04:17 UTC