From e04ee2431eb3d65ce511d109d5f709f087622b9a Mon Sep 17 00:00:00 2001 From: Nima Rasekh Date: Sat, 24 May 2025 20:24:07 +0200 Subject: [PATCH] Fix typo --- MIL/C07_Hierarchies/S01_Basics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean index 4a273cc..0a59d31 100644 --- a/MIL/C07_Hierarchies/S01_Basics.lean +++ b/MIL/C07_Hierarchies/S01_Basics.lean @@ -120,7 +120,7 @@ class Semigroup₀ (α : Type) where Note that while stating `dia_assoc`, the previously defined field `toDia₁` is in the local context hence can be used when Lean searches for an instance of `Dia₁ α` to make sense of `a ⋄ b`. However this `toDia₁` field does not become part of the type class instances database. -Hence doing ``example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b`` would fail with +Hence doing ``example {α : Type} [Semigroup₀ α] (a b : α) : α := a ⋄ b`` would fail with error message ``failed to synthesize instance Dia₁ α``. We can fix this by adding the ``instance`` attribute later.