From 64eeba726a63212aff0c89e067030b2425e8122f Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 7 Jul 2024 22:31:35 +1000
Subject: [PATCH] chore: make Antisymm a Prop (#4666)

As pointed out on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Antisymm.60.20is.20in.20.60Type.60/near/449084812).
---
 src/Init/Core.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 309e9774f429..9438d4724970 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1867,7 +1867,7 @@ instance : Subsingleton (Squash α) where
 /--
 `Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
 -/
-class Antisymm {α : Sort u} (r : α → α → Prop) where
+class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
   antisymm {a b : α} : r a b → r b a → a = b