Balazs Toth (Dec 13 2023 at 13:02): Balazs Toth (Dec 13 2023 at 13:02):Hello,
I am instantiating a locale like this:
sublocale some_locale arg1 arg2 arg3
proof
...
qed
Which contains definitions etc. When I now want to use one of the definitions, their type signature contains a ??'a itself ⇒in the front. What can be the reason for this? And what is an itself?
I used locales in a very similiar way in other places and did not have this issue.
Lukas Stevens (Dec 13 2023 at 14:19):itself is a type constructor that takes a type to itself. You can obtain an 'a itself by writing TYPE('a). This occurs if your definition depends on a type that does not occur in any of the argument types.
Balazs Toth (Dec 13 2023 at 14:20):Ahh, I see, thanks :)
Lukas Stevens (Dec 13 2023 at 14:21):Very contrived example
definition "f (x :: 'a) ≡ (undefined :: 'b ⇒ 'a) ((undefined :: 'a ⇒ 'b) x)"
Last updated: Nov 13 2025 at 04:27 UTC