From 44985dc9a64bb6f4f898abb7be24e7be47f42bb7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 29 Aug 2024 15:18:44 +1000 Subject: [PATCH] chore: remove >6 month deprecations (#5199) --- src/Init/Data/BitVec/Lemmas.lean | 3 --- src/Init/Data/Bool.lean | 3 --- src/Init/Data/Fin/Lemmas.lean | 3 --- src/Init/Data/Nat/Lemmas.lean | 16 ---------------- src/Lean/Meta/Tactic/Replace.lean | 4 ---- src/Lean/Widget/UserWidget.lean | 18 ------------------ 6 files changed, 47 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 5bbaa37d78..b43d1e4360 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -152,9 +152,6 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) : getLsb (BitVec.ofNat n x) i = (i < n && x.testBit i) := by simp [getLsb, BitVec.ofNat, Fin.val_ofNat'] -@[simp, deprecated toNat_ofNat (since := "2024-02-22")] -theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial - @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb] @[simp] theorem getMsb_zero : (0#w).getMsb i = false := by simp [getMsb] diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 60f58f58c9..44304303b5 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -381,9 +381,6 @@ def toNat (b : Bool) : Nat := cond b 1 0 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by cases c <;> trivial -@[deprecated toNat_le (since := "2024-02-23")] -abbrev toNat_le_one := toNat_le - theorem toNat_lt (b : Bool) : b.toNat < 2 := Nat.lt_succ_of_le (toNat_le _) diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index c13120c883..2ee40b879b 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -54,9 +54,6 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta .. @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) : (Fin.ofNat' a is_pos).val = a % n := rfl -@[deprecated ofNat'_zero_val (since := "2024-02-22")] -theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _ - @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val := rfl diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index f0d739f457..d958f0898b 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -157,17 +157,9 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m := ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩ -@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")] -protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m := - (Nat.le_sub_iff_add_le h).symm - protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k := Nat.add_comm .. ▸ Nat.add_le_of_le_sub h -@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")] -protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k := - Nat.add_le_of_le_sub' h - protected theorem le_sub_of_add_le' {n k m : Nat} : m + n ≤ k → n ≤ k - m := Nat.add_comm .. ▸ Nat.le_sub_of_add_le @@ -429,14 +421,6 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min /-! ### mul -/ -@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")] -protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b := - Nat.mul_le_mul_left c - -@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")] -protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c := - Nat.mul_le_mul_right c - protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by rw [Nat.mul_assoc, Nat.mul_comm m, ← Nat.mul_assoc] diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index be9c73fad4..ec5099258e 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -190,10 +190,6 @@ def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (type | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target" return mvarId -@[deprecated MVarId.changeLocalDecl (since := "2022-07-15")] -def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do - mvarId.changeLocalDecl fvarId typeNew checkDefEq - /-- Modify `mvarId` target type using `f`. -/ diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 7de9019f95..bb71e6e67e 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -357,15 +357,6 @@ structure UserWidgetDefinition where instance : ToModule UserWidgetDefinition where toModule uwd := { uwd with } -@[deprecated (since := "2023-12-21")] private def widgetAttrImpl : AttributeImpl where - name := `widget - descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead." - applicationTime := AttributeApplicationTime.afterCompilation - add := widgetModuleAttrImpl.add - -set_option linter.deprecated false in -builtin_initialize registerBuiltinAttribute widgetAttrImpl - private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] (id : Name) : m UserWidgetDefinition := do ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id @@ -374,13 +365,6 @@ private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadO opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m] (id : Name) : m UserWidgetDefinition -/-- Save a user-widget instance to the infotree. - The given `widgetId` should be the declaration name of the widget definition. -/ -@[deprecated savePanelWidgetInfo (since := "2023-12-21")] def saveWidgetInfo (widgetId : Name) (props : Json) - (stx : Syntax) : CoreM Unit := do - let uwd ← evalUserWidgetDefinition widgetId - savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx - /-! ## Retrieving panel widget instances -/ /-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/ @@ -447,6 +431,4 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp builtin_initialize Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets -attribute [deprecated Module (since := "2023-12-21")] UserWidgetDefinition - end Lean.Widget