Skip to content

Commit

Permalink
chore: remove >6 month old deprecations (#1044)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Nov 13, 2024
1 parent 6d0acd1 commit e2b30dc
Show file tree
Hide file tree
Showing 9 changed files with 0 additions and 116 deletions.
2 changes: 0 additions & 2 deletions Batteries.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ import Batteries.Data.UInt
import Batteries.Data.UnionFind
import Batteries.Data.Vector
import Batteries.Lean.AttributeExtra
import Batteries.Lean.Delaborator
import Batteries.Lean.EStateM
import Batteries.Lean.Except
import Batteries.Lean.Expr
Expand Down Expand Up @@ -70,7 +69,6 @@ import Batteries.Linter
import Batteries.Linter.UnnecessarySeqFocus
import Batteries.Linter.UnreachableTactic
import Batteries.Logic
import Batteries.StdDeprecations
import Batteries.Tactic.Alias
import Batteries.Tactic.Basic
import Batteries.Tactic.Case
Expand Down
17 changes: 0 additions & 17 deletions Batteries/Data/Array/Merge.lean
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,6 @@ where
if lt x y then go (acc.push x) (i + 1) j else go (acc.push y) i (j + 1)
termination_by xs.size + ys.size - (i + j)

set_option linter.unusedVariables false in
@[deprecated merge (since := "2024-04-24"), inherit_doc merge]
def mergeSortedPreservingDuplicates [ord : Ord α] (xs ys : Array α) : Array α :=
merge (compare · · |>.isLT) xs ys

-- We name `ord` so it can be provided as a named argument.
set_option linter.unusedVariables.funArgs false in
/--
Expand All @@ -57,17 +52,13 @@ where
| .eq => go (acc.push (merge x y)) (i + 1) (j + 1)
termination_by xs.size + ys.size - (i + j)

@[deprecated (since := "2024-04-24")] alias mergeSortedMergingDuplicates := mergeDedupWith

/--
`O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
not contain duplicates. If an element appears in both `xs` and `ys`, only one copy is kept.
-/
@[inline] def mergeDedup [ord : Ord α] (xs ys : Array α) : Array α :=
mergeDedupWith (ord := ord) xs ys fun x _ => x

@[deprecated (since := "2024-04-24")] alias mergeSortedDeduplicating := mergeDedup

set_option linter.unusedVariables false in
/--
`O(|xs| * |ys|)`. Merge `xs` and `ys`, which do not need to be sorted. Elements which occur in
Expand All @@ -85,8 +76,6 @@ where
ys.foldl (init := xs) fun xs y =>
if xs.any (· == y) (stop := xsSize) then xs else xs.push y

@[deprecated (since := "2024-04-24")] alias mergeUnsortedDeduplicating := mergeUnsortedDedup

-- We name `eq` so it can be provided as a named argument.
set_option linter.unusedVariables.funArgs false in
/--
Expand All @@ -105,22 +94,16 @@ where
acc.push hd
termination_by xs.size - i

@[deprecated (since := "2024-04-24")] alias mergeAdjacentDuplicates := mergeAdjacentDups

/--
`O(|xs|)`. Deduplicate a sorted array. The array must be sorted with to an order which agrees with
`==`, i.e. whenever `x == y` then `compare x y == .eq`.
-/
def dedupSorted [eq : BEq α] (xs : Array α) : Array α :=
xs.mergeAdjacentDups (eq := eq) fun x _ => x

@[deprecated (since := "2024-04-24")] alias deduplicateSorted := dedupSorted

/-- `O(|xs| log |xs|)`. Sort and deduplicate an array. -/
def sortDedup [ord : Ord α] (xs : Array α) : Array α :=
have := ord.toBEq
dedupSorted <| xs.qsort (compare · · |>.isLT)

@[deprecated (since := "2024-04-24")] alias sortAndDeduplicate := sortDedup

end Array
4 changes: 0 additions & 4 deletions Batteries/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -53,10 +53,6 @@ drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
| [] => []
| x :: xs => bif p x then xs else after p xs

@[deprecated (since := "2024-05-06")] alias removeNth := eraseIdx
@[deprecated (since := "2024-05-06")] alias removeNthTR := eraseIdxTR
@[deprecated (since := "2024-05-06")] alias removeNth_eq_removeNthTR := eraseIdx_eq_eraseIdxTR

/-- Replaces the first element of the list for which `f` returns `some` with the returned value. -/
@[simp] def replaceF (f : α → Option α) : List α → List α
| [] => []
Expand Down
3 changes: 0 additions & 3 deletions Batteries/Data/List/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -524,7 +524,6 @@ theorem get?_inj
@[deprecated (since := "2024-10-21")] alias modifyNth_succ_cons := modify_succ_cons
@[deprecated (since := "2024-10-21")] alias modifyNthTail_id := modifyTailIdx_id
@[deprecated (since := "2024-10-21")] alias eraseIdx_eq_modifyNthTail := eraseIdx_eq_modifyTailIdx
@[deprecated (since := "2024-05-06")] alias removeNth_eq_nth_tail := eraseIdx_eq_modifyTailIdx
@[deprecated (since := "2024-10-21")] alias getElem?_modifyNth := getElem?_modify
@[deprecated getElem?_modify (since := "2024-06-12")]
theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) :
Expand Down Expand Up @@ -574,5 +573,3 @@ theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get
theorem get?_set (a : α) {m n} (l : List α) :
(set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n := by
simp [getElem?_set']; rfl
@[deprecated (since := "2024-05-06")] alias length_removeNth := length_eraseIdx
@[deprecated (since := "2024-04-22")] alias sublist.erase := Sublist.erase
9 changes: 0 additions & 9 deletions Batteries/Data/RBMap/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -67,9 +67,6 @@ protected def max? : RBNode α → Option α
| node _ _ v nil => some v
| node _ _ _ r => r.max?

@[deprecated (since := "2024-04-17")] protected alias min := RBNode.min?
@[deprecated (since := "2024-04-17")] protected alias max := RBNode.max?

/--
Fold a function in tree order along the nodes. `v₀` is used at `nil` nodes and
`f` is used to combine results at branching nodes.
Expand Down Expand Up @@ -670,9 +667,6 @@ instance : ToStream (RBSet α cmp) (RBNode.Stream α) := ⟨fun x => x.1.toStrea
/-- `O(log n)`. Returns the entry `a` such that `a ≥ k` for all keys in the RBSet. -/
@[inline] protected def max? (t : RBSet α cmp) : Option α := t.1.max?

@[deprecated (since := "2024-04-17")] protected alias min := RBSet.min?
@[deprecated (since := "2024-04-17")] protected alias max := RBSet.max?

instance [Repr α] : Repr (RBSet α cmp) where
reprPrec m prec := Repr.addAppParen ("RBSet.ofList " ++ repr m.toList) prec

Expand Down Expand Up @@ -1055,9 +1049,6 @@ instance : Stream (Values.Stream α β) β := ⟨Values.Stream.next?⟩
/-- `O(log n)`. Returns the key-value pair `(a, b)` such that `a ≥ k` for all keys in the RBMap. -/
@[inline] protected def max? : RBMap α β cmp → Option (α × β) := RBSet.max?

@[deprecated (since := "2024-04-17")] protected alias min := RBMap.min?
@[deprecated (since := "2024-04-17")] protected alias max := RBMap.max?

instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
reprPrec m prec := Repr.addAppParen ("RBMap.ofList " ++ repr m.toList) prec

Expand Down
13 changes: 0 additions & 13 deletions Batteries/Lean/Delaborator.lean

This file was deleted.

3 changes: 0 additions & 3 deletions Batteries/Lean/HashSet.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,6 @@ namespace Std.HashSet

variable [BEq α] [Hashable α]

instance : Singleton α (HashSet α) := ⟨fun x => HashSet.empty.insert x⟩
instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩

/--
`O(n)`. Returns `true` if `f` returns `true` for any element of the set.
-/
Expand Down
2 changes: 0 additions & 2 deletions Batteries/Logic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ import Batteries.Tactic.Alias
instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
inferInstanceAs <| DecidablePred fun x => p (f x)

@[deprecated (since := "2024-03-15")] alias proofIrrel := proof_irrel

/-! ## id -/

theorem Function.id_def : @id α = fun x => x := rfl
Expand Down
63 changes: 0 additions & 63 deletions Batteries/StdDeprecations.lean

This file was deleted.

0 comments on commit e2b30dc

Please sign in to comment.