deprecations

leanprover-community · Oct 12, 2024 · c17bf63 · c17bf63
1 parent cc9d992
commit c17bf63
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/Mathlib/SetTheory/Surreal/Basic.lean b/Mathlib/SetTheory/Surreal/Basic.lean
@@ -244,6 +244,12 @@ theorem insertRight {x x' : PGame} (x_num : x.Numeric) (x'_num : x'.Numeric)
 
 end Numeric
 
+@[deprecated Numeric.insertLeft (since := "2024-10-11")]
+alias insertLeft_numeric := Numeric.insertLeft
+
+@[deprecated Numeric.insertRight (since := "2024-10-11")]
+alias insertRight_numeric := Numeric.insertRight
+
 /-- Pre-games defined by natural numbers are numeric. -/
 theorem numeric_nat : ∀ n : ℕ, Numeric n
   | 0 => numeric_zero