Gergely Buday (Feb 07 2025 at 16:34): Gergely Buday (Feb 07 2025 at 16:34):I have the following example:
locale simple = fixes a :: "'A"
locale complex =
Alpha: simple A + Beta: simple B
for A B +
fixes f :: "Alpha.a ⇒ Beta.a"
How can I refer to Alpha's 'A type? In a more detailed example I could use the generated type variables after the for clause, but I think in general it is not recommended to rely on generated variable or type names.
For the above I get this error message:
Undefined type name: "Alpha.a"⌂
Failed to parse type
I tried with Alpha.'A but it also did not work.
Mathias Fleury (Feb 07 2025 at 16:42):I would go for
locale complex =
Alpha: simple A + Beta: simple B
for A :: "'A" and B :: "'B" +
fixes f :: "'A ⇒ 'B"
Follow-up question: in the body of the complex locale, how could I refer to 'A and 'B? ChatGPT says this is not possible, I am not sure if it is right saying so.
Gergely Buday (Feb 10 2025 at 13:58):As the body I mean the part after begin
Gergely Buday (Feb 10 2025 at 14:45):Interestingly, I can use it in a definition:
locale simple = fixes a :: "'A"
locale complex =
Alpha: simple A + Beta: simple B
for A :: "'A" and B :: "'B"
begin
definition foo :: "'A"
where "foo = A"
value "foo"
and value correctly reports 'A as the type of foo, but I cannot fix the following in the body:
datatype A2 = Foo | Original (the: 'A)
Isabelle tells me that 'A is a type variable, not a type that I could use in a datatype definition:
Extra type variables on right-hand side: "'A"
How could I refer to locale Alpha's 'A type variable for my datatype?
If I try give 'A as a type variable:
datatype 'A A2 = Foo string | Original (the: 'A)
then I get this error message:
Locally fixed type argument "'A" in datatype specification
I'm confused then, what "'A" is.
Gergely Buday (Feb 10 2025 at 16:31):ANSWER:
says that I should define my datatype outside of locales
Last updated: Nov 07 2025 at 16:23 UTC