From 1db0bca914af2bfe3e4f3289124e505823ebae94 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Fri, 2 Jul 2021 06:43:35 -0400 Subject: [PATCH] fix: protect `Equiv` --- src/Init/Core.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index e9fc1bb32b..e3219164b3 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -944,15 +944,15 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] namespace Function variable {α : Sort u} {β : α → Sort v} -def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x +protected def Equiv (f₁ f₂ : ∀ (x : α), β x) : Prop := ∀ x, f₁ x = f₂ x -protected theorem Equiv.refl (f : ∀ (x : α), β x) : Equiv f f := +protected theorem Equiv.refl (f : ∀ (x : α), β x) : Function.Equiv f f := fun x => rfl -protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₁ := +protected theorem Equiv.symm {f₁ f₂ : ∀ (x : α), β x} : Function.Equiv f₁ f₂ → Function.Equiv f₂ f₁ := fun h x => Eq.symm (h x) -protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ := +protected theorem Equiv.trans {f₁ f₂ f₃ : ∀ (x : α), β x} : Function.Equiv f₁ f₂ → Function.Equiv f₂ f₃ → Function.Equiv f₁ f₃ := fun h₁ h₂ x => Eq.trans (h₁ x) (h₂ x) protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) := {