update lean

1 files changed, 4 insertions, 8 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index e03d67a..f1a711b 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -225,16 +225,12 @@ instance NameAbstraction.setoid_equivariant : Rel.Equivariant 𝔸 (setoid 𝔸
   instAlphaEqEquivariant
 
 /-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
-def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
+abbrev NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
 
 namespace NameAbstraction
 
-/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
-abbrev mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
-  Quotient.mk (setoid 𝔸 X) (.mk a x)
-
 /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
-notation "⟪" a "⟫ " x:60 => mk a x
+notation "⟪" a "⟫ " x:60 => (⟦⟨a, x⟩⟧ : NameAbstraction _ _)
 
 instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸
 
@@ -390,13 +386,13 @@ private lemma map_id : map 𝔸 (EquivariantMap.id 𝔸 : X →ₑ[𝔸] X) = Eq
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.id 𝔸) x = x by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 private lemma map_comp (f : Y →ₑ[𝔸] Z) (g : X →ₑ[𝔸] Y) : map 𝔸 (EquivariantMap.comp 𝔸 f g) = EquivariantMap.comp 𝔸 (map 𝔸 f) (map 𝔸 g) := by
   suffices ∀ (x : NameAbstraction 𝔸 X), map' 𝔸 (EquivariantMap.comp 𝔸 f g) x = (map' 𝔸 f) ((map' 𝔸 g) x) by ext x; exact this x
   apply Quotient.ind
   intro x
-  simp [map', NameAbstraction.mk]
+  simp [map']
 
 /-- Name abstractions form a functor `Nom ⥤ Nom`. -/
 def Functor : Nom 𝔸 ⥤ Nom 𝔸 :=