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?
No (see https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00106.html)
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).
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: Dec 07 2023 at 20:16 UTC