Julin Shaji (Feb 13 2025 at 16:44): Julin Shaji (Feb 13 2025 at 16:44):I was trying to replicate an example mentioned in this document:
https://isabelle.in.tum.de/doc/classes.pdf
theory Semigroup
imports Main
begin
class semigroup =
fixes mult :: ‹α ⇒ α ⇒ α› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
end
But jedit gives error in the fixes mult line:
Undefined type name: "α"⌂
Failed to parse type
Where did I go wrong?
I suppose I need to somehow declare α?
How can that be done?
Julin Shaji (Feb 13 2025 at 16:47):Also tried ∷ instead of :: like
class semigroup =
fixes mult ∷ ‹α ⇒ α ⇒ α› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
but that gave this error:
Outer syntax error⌂: command expected,
but text cartouche⌂ was found:
‹α ⇒ α ⇒ α
Oh never mind.
Using 'a instead of alpha worked.
class semigroup =
fixes mult :: ‹'a ⇒ 'a ⇒ 'a› (infixl ‹⊗› 70)
assumes assoc : ‹(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)›
I have always read (and see people read) 'a as alpha, 'b as beta and so one…
Last updated: Mar 09 2025 at 12:28 UTC