From 2688d88ecb9e181151ac21b7d7f7dab5cb464d89 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 24 May 2026 19:30:28 -0600 Subject: [PATCH 1/2] 3 --- Mathlib/SetTheory/Ordinal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 3ae32b127dfa6e..803140f1075b06 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -146,7 +146,7 @@ def type (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal := ⟦⟨α, r, wo⟩⟧ /-- `typeLT α` is an abbreviation for the order type of the `<` relation of `α`. -/ -scoped notation "typeLT " α:70 => @Ordinal.type α (· < ·) inferInstance +scoped notation3 "typeLT " α:70 => @Ordinal.type α (· < ·) inferInstance instance zero : Zero Ordinal := ⟨type <| @emptyRelation PEmpty⟩ From d21f60a08869da91318ca7251a5d12587d8b552f Mon Sep 17 00:00:00 2001 From: vihdzp Date: Mon, 25 May 2026 15:56:13 -0600 Subject: [PATCH 2/2] guardmsgs --- Mathlib/SetTheory/Ordinal/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 803140f1075b06..0ca86d8727d732 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -148,6 +148,10 @@ def type (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal := /-- `typeLT α` is an abbreviation for the order type of the `<` relation of `α`. -/ scoped notation3 "typeLT " α:70 => @Ordinal.type α (· < ·) inferInstance +/-- info: typeLT ℕ : Ordinal.{0} -/ +#guard_msgs in +#check typeLT ℕ + instance zero : Zero Ordinal := ⟨type <| @emptyRelation PEmpty⟩