Update Core.lean

leanprover · Jan 15, 2025 · 71ffdb9 · 71ffdb9
1 parent a7597d1
commit 71ffdb9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -1913,7 +1913,7 @@ theorem true_equivalence (α : Sort u) : Equivalence fun _ _ : α ↦ True :=
 
 /-- Always-true relation as a `Setoid`. -/
 def trueSetoid (α : Sort u) : Setoid α :=
-  ⟨_, true_equivalence⟩
+  ⟨_, true_equivalence α⟩
 
 /--
 `Squash α` is the quotient of `α` by the always true relation.