/- Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul Reichert -/ import Std.Data.TreeSet.Basic import Std.Data.TreeSet.Lemmas import Std.Data.TreeSet.Raw.Basic import Std.Data.DTreeMap.Raw.AdditionalOperations import Std.Data.TreeMap.Raw.AdditionalOperations import Std.Data.TreeMap.AdditionalOperations import Std.Data.DTreeMap.Iterator import Std.Data.DTreeMap.Raw.Iterator import Std.Data.DTreeMap.Slice import Std.Data.DTreeMap.Raw.Slice import Std.Data.TreeMap.Iterator import Std.Data.TreeMap.Raw.Iterator import Std.Data.TreeMap.Slice import Std.Data.TreeMap.Raw.Slice import Std.Data.TreeSet.Iterator import Std.Data.TreeSet.Raw.Iterator import Std.Data.TreeSet.Slice import Std.Data.TreeSet.Raw.Slice open Std variable {α : Type u} {β : Type v} [Ord α] def mkDTreeMapSingleton (a : α) (b : β) : DTreeMap α (fun _ => β) := Id.run do let mut m : DTreeMap α (fun _ => β) := ∅ m := m.insert a b return m def mkTreeMapSingleton (a : α) (b : β) : TreeMap α β := Id.run do let mut m : TreeMap α β := ∅ m := m.insert a b return m def mkTreeSetSingleton (a : α) : TreeSet α := Id.run do let mut m : TreeSet α := ∅ m := m.insert a return m example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := mkDTreeMapSingleton a b |>.get? a example [TransOrd α] [LawfulEqOrd α] (a : α) (b : β) : Option β := (mkTreeMapSingleton a b)[a]? example [TransOrd α] (a : α) (b : β) : (mkTreeMapSingleton a b).contains a := by simp [mkTreeMapSingleton] example [TransOrd α] (a : α) (b : β) : (mkDTreeMapSingleton a b).contains a := by simp [mkDTreeMapSingleton] example [TransOrd α] (a : α) : (mkTreeSetSingleton a).contains a := by simp [mkTreeSetSingleton] namespace DTreeMap.Raw def t : DTreeMap.Raw Nat (fun _ => Nat) := .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] /-- info: [⟨2, 8⟩] -/ #guard_msgs in #eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/ #guard_msgs in #eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [⟨3, 6⟩] -/ #guard_msgs in #eval (t.filter fun _ v => v > 4).toList /-- info: [(3, 6), (2, 4), (1, 2)] -/ #guard_msgs in #eval Id.run do let mut ans : List (Nat × Nat) := [] for ⟨k, v⟩ in t do ans := (k, v) :: ans return ans /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.toList /-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.toArray /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DTreeMap.Raw.Const.toList t /-- info: #[(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DTreeMap.Raw.Const.toArray t /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keys /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.keysArray /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.values /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DTreeMap.Raw.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList /-- info: Std.DTreeMap.Raw.ofList [⟨1, 4⟩] -/ #guard_msgs in #eval DTreeMap.Raw.Const.ofList [(1, 2), (1, 4)] local instance : Inhabited ((_ : Nat) × Nat) where default := ⟨0, 0⟩ /-- info: some ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdx? 1 /-- info: some (2, 4) -/ #guard_msgs in #eval DTreeMap.Raw.Const.entryAtIdx? t 1 /-- info: none -/ #guard_msgs in #eval t.entryAtIdx? 3 /-- info: none -/ #guard_msgs in #eval DTreeMap.Raw.Const.entryAtIdx? t 3 /-- info: ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdx! 1 /-- info: (2, 4) -/ #guard_msgs in #eval DTreeMap.Raw.Const.entryAtIdx! t 1 /-- info: ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdxD 1 ⟨42, 3⟩ /-- info: (2, 4) -/ #guard_msgs in #eval DTreeMap.Raw.Const.entryAtIdxD t 1 ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval t.entryAtIdxD 3 ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval DTreeMap.Raw.Const.entryAtIdxD t 3 ⟨42, 3⟩ -- TODO: keyAtIdx /-- info: some 2 -/ #guard_msgs in #eval t.keyAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.keyAtIdx? 3 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.keyAtIdxD 3 42 /-- info: [none, none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x /-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLT? t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getEntryLT! x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLT! t x /-- info: [⟨42, 3⟩, ⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩ /-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLTD t x (42, 3) /-- info: [none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, some ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x /-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLE? t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getEntryLE! x /-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLE! t x /-- info: [⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩ /-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryLED t x ⟨42, 3⟩ /-- info: [some ⟨1, 2⟩, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x /-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGE? t x /-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getEntryGE! x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => DTreeMap.Raw.Const.getEntryGE! t x /-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩ /-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGED t x ⟨42, 3⟩ /-- info: [some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x /-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGT? t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getEntryGT! x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2].map fun x => DTreeMap.Raw.Const.getEntryGT! t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩, ⟨42, 3⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩ /-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Raw.Const.getEntryGTD t x ⟨42, 3⟩ /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getKeyLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getKeyLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getKeyGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getKeyGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42 /-- info: some ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntry? /-- info: some (1, 2) -/ #guard_msgs in #eval DTreeMap.Raw.Const.minEntry? t /-- info: none -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntry? /-- info: none -/ #guard_msgs in #eval DTreeMap.Raw.Const.minEntry? (∅ : DTreeMap.Raw Nat fun _ => Nat) /-- info: ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntry! /-- info: (1, 2) -/ #guard_msgs in #eval DTreeMap.Raw.Const.minEntry! t /-- info: ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntryD ⟨42, 3⟩ /-- info: (1, 2) -/ #guard_msgs in #eval DTreeMap.Raw.Const.minEntryD t ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval DTreeMap.Raw.Const.minEntryD (∅ : DTreeMap.Raw Nat fun _ => Nat) ⟨42, 3⟩ /-- info: some ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntry? /-- info: some (3, 6) -/ #guard_msgs in #eval DTreeMap.Raw.Const.maxEntry? t /-- info: none -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntry? /-- info: none -/ #guard_msgs in #eval DTreeMap.Raw.Const.maxEntry? (∅ : DTreeMap.Raw Nat fun _ => Nat) /-- info: ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntry! /-- info: (3, 6) -/ #guard_msgs in #eval DTreeMap.Raw.Const.maxEntry! t /-- info: ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntryD ⟨42, 3⟩ /-- info: (3, 6) -/ #guard_msgs in #eval DTreeMap.Raw.Const.maxEntryD t ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntryD ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval DTreeMap.Raw.maxEntryD (∅ : DTreeMap.Raw Nat fun _ => Nat) ⟨42, 3⟩ /-- info: (Std.DTreeMap.Raw.ofList [⟨3, 6⟩], Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩]) -/ #guard_msgs in #eval t.partition fun k v => k + 3 == v /-- info: (Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩], Std.DTreeMap.Raw.ofList []) -/ #guard_msgs in #eval t.partition fun _ _ => true /-- info: (Std.DTreeMap.Raw.ofList [], Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]) -/ #guard_msgs in #eval t.partition fun _ _ => false /-- info: (Std.DTreeMap.Raw.ofList [], Std.DTreeMap.Raw.ofList []) -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).partition fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun k v => k + 5 == v /-- info: false -/ #guard_msgs in #eval t.all fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k v => k + k == v /-- info: false -/ #guard_msgs in #eval t.all fun k v => k + 3 == v /-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.DTreeMap.Raw.ofList [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.DTreeMap.Raw.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] -- We can't prove the non-Const variant yet because Nat doesn't have a LawfulEqOrd instance /-- info: Std.DTreeMap.Raw.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval DTreeMap.Raw.Const.mergeWith (fun _ v _ => v) t ∅ /-- info: Std.DTreeMap.Raw.ofList [⟨0, 0⟩, ⟨1, 0⟩, ⟨2, 0⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval DTreeMap.Raw.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩]) /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keysIter.toList /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.valuesIter.toList /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[*...*].toList /-- info: [⟨1, 2⟩, ⟨2, 4⟩] -/ #guard_msgs in #eval t[*...=2].toList /-- info: [⟨1, 2⟩] -/ #guard_msgs in #eval t[*...<2].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[2...*].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[2...=3].toList /-- info: [⟨2, 4⟩] -/ #guard_msgs in #eval t[2...<3].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[1<...*].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[1<...=3].toList /-- info: [⟨2, 4⟩] -/ #guard_msgs in #eval t[1<...<3].toList end DTreeMap.Raw namespace DTreeMap def t : DTreeMap Nat (fun _ => Nat) := .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] /-- info: [⟨2, 8⟩] -/ #guard_msgs in #eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/ #guard_msgs in #eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [⟨3, 6⟩] -/ #guard_msgs in #eval (t.filter fun _ v => v > 4).toList /-- info: [(3, 6), (2, 4), (1, 2)] -/ #guard_msgs in #eval Id.run do let mut ans : List (Nat × Nat) := [] for ⟨k, v⟩ in t do ans := (k, v) :: ans return ans /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.toList /-- info: #[⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.toArray /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DTreeMap.Const.toList t /-- info: #[(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DTreeMap.Const.toArray t /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keys /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.keysArray /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.values /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DTreeMap.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList /-- info: Std.DTreeMap.ofList [⟨1, 4⟩] -/ #guard_msgs in #eval DTreeMap.Const.ofList [(1, 2), (1, 4)] local instance : Inhabited ((_ : Nat) × Nat) where default := ⟨0, 0⟩ /-- info: some ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdx? 1 /-- info: some (2, 4) -/ #guard_msgs in #eval DTreeMap.Const.entryAtIdx? t 1 /-- info: ⟨2, 4⟩ --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.entryAtIdx 1 sorry /-- info: (2, 4) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! DTreeMap.Const.entryAtIdx t 1 sorry /-- info: none -/ #guard_msgs in #eval t.entryAtIdx? 3 /-- info: none -/ #guard_msgs in #eval DTreeMap.Const.entryAtIdx? t 3 /-- info: ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdx! 1 /-- info: (2, 4) -/ #guard_msgs in #eval DTreeMap.Const.entryAtIdx! t 1 /-- info: ⟨2, 4⟩ -/ #guard_msgs in #eval t.entryAtIdxD 1 ⟨42, 3⟩ /-- info: (2, 4) -/ #guard_msgs in #eval DTreeMap.Const.entryAtIdxD t 1 ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval t.entryAtIdxD 3 ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval DTreeMap.Const.entryAtIdxD t 3 ⟨42, 3⟩ /-- info: some 2 -/ #guard_msgs in #eval t.keyAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.keyAtIdx? 3 /-- info: 2 --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.keyAtIdx 1 sorry /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.keyAtIdxD 3 42 /-- info: [none, none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x /-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLT? t x /- Cannot test `getEntryLT` etc. as of writing (2025-03-25) because `TransOrd Nat` is not implemented yet. -/ /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getEntryLT! x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [2, 3, 4].map fun x => DTreeMap.Const.getEntryLT! t x /-- info: [⟨42, 3⟩, ⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩ /-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLTD t x (42, 3) /-- info: [none, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, some ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x /-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLE? t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getEntryLE! x /-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLE! t x /-- info: [⟨42, 3⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩ /-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryLED t x ⟨42, 3⟩ /-- info: [some ⟨1, 2⟩, some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x /-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGE? t x /-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getEntryGE! x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => DTreeMap.Const.getEntryGE! t x /-- info: [⟨1, 2⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩ /-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGED t x ⟨42, 3⟩ /-- info: [some ⟨1, 2⟩, some ⟨2, 4⟩, some ⟨3, 6⟩, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x /-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGT? t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getEntryGT! x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2].map fun x => DTreeMap.Const.getEntryGT! t x /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩, ⟨42, 3⟩, ⟨42, 3⟩] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩ /-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => DTreeMap.Const.getEntryGTD t x ⟨42, 3⟩ /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getKeyLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getKeyLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getKeyGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getKeyGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42 /-- info: some ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntry? /-- info: some (1, 2) -/ #guard_msgs in #eval DTreeMap.Const.minEntry? t /-- info: ⟨1, 2⟩ --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.minEntry sorry /-- info: (1, 2) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! DTreeMap.Const.minEntry t sorry /-- info: none -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntry? /-- info: none -/ #guard_msgs in #eval DTreeMap.Const.minEntry? (∅ : DTreeMap Nat fun _ => Nat) /-- info: ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntry! /-- info: (1, 2) -/ #guard_msgs in #eval DTreeMap.Const.minEntry! t /-- info: ⟨1, 2⟩ -/ #guard_msgs in #eval t.minEntryD ⟨42, 3⟩ /-- info: (1, 2) -/ #guard_msgs in #eval DTreeMap.Const.minEntryD t ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).minEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval DTreeMap.Const.minEntryD (∅ : DTreeMap Nat fun _ => Nat) ⟨42, 3⟩ /-- info: some ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntry? /-- info: some (3, 6) -/ #guard_msgs in #eval DTreeMap.Const.maxEntry? t /-- info: ⟨3, 6⟩ --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.maxEntry sorry /-- info: (3, 6) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! DTreeMap.Const.maxEntry t sorry /-- info: none -/ #guard_msgs in #eval (∅ : DTreeMap Nat fun _ => Nat).maxEntry? /-- info: none -/ #guard_msgs in #eval DTreeMap.Const.maxEntry? (∅ : DTreeMap Nat fun _ => Nat) /-- info: ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntry! /-- info: (3, 6) -/ #guard_msgs in #eval DTreeMap.Const.maxEntry! t /-- info: ⟨3, 6⟩ -/ #guard_msgs in #eval t.maxEntryD ⟨42, 3⟩ /-- info: (3, 6) -/ #guard_msgs in #eval DTreeMap.Const.maxEntryD t ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval (∅ : DTreeMap.Raw Nat fun _ => Nat).maxEntryD ⟨42, 3⟩ /-- info: ⟨42, 3⟩ -/ #guard_msgs in #eval DTreeMap.maxEntryD (∅ : DTreeMap Nat fun _ => Nat) ⟨42, 3⟩ /-- info: (Std.DTreeMap.ofList [⟨3, 6⟩], Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩]) -/ #guard_msgs in #eval t.partition fun k v => k + 3 == v /-- info: (Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩], Std.DTreeMap.ofList []) -/ #guard_msgs in #eval t.partition fun _ _ => true /-- info: (Std.DTreeMap.ofList [], Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩]) -/ #guard_msgs in #eval t.partition fun _ _ => false /-- info: (Std.DTreeMap.ofList [], Std.DTreeMap.ofList []) -/ #guard_msgs in #eval (∅ : DTreeMap Nat fun _ => Nat).partition fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun k v => k + 5 == v /-- info: false -/ #guard_msgs in #eval t.all fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k v => k + k == v /-- info: false -/ #guard_msgs in #eval t.all fun k v => k + 3 == v /-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.DTreeMap.ofList [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.DTreeMap.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] -- We can't prove the non-Const variant yet because Nat doesn't have a LawfulEqOrd instance /-- info: Std.DTreeMap.ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval DTreeMap.Const.mergeWith (fun _ v _ => v) t ∅ /-- info: Std.DTreeMap.ofList [⟨0, 0⟩, ⟨1, 0⟩, ⟨2, 0⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval DTreeMap.Const.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩]) /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keysIter.toList /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.valuesIter.toList /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keysIter.toList /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.valuesIter.toList /-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[*...*].toList /-- info: [⟨1, 2⟩, ⟨2, 4⟩] -/ #guard_msgs in #eval t[*...=2].toList /-- info: [⟨1, 2⟩] -/ #guard_msgs in #eval t[*...<2].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[2...*].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[2...=3].toList /-- info: [⟨2, 4⟩] -/ #guard_msgs in #eval t[2...<3].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[1<...*].toList /-- info: [⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval t[1<...=3].toList /-- info: [⟨2, 4⟩] -/ #guard_msgs in #eval t[1<...<3].toList end DTreeMap namespace TreeMap.Raw def t : TreeMap.Raw Nat Nat := .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] /-- info: [(2, 8)] -/ #guard_msgs in #eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [(1, none), (2, some 8), (3, none)] -/ #guard_msgs in #eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [(3, 6)] -/ #guard_msgs in #eval (t.filter fun _ v => v > 4).toList /-- info: [(3, 6), (2, 4), (1, 2)] -/ #guard_msgs in #eval Id.run do let mut ans : List (Nat × Nat) := [] for ⟨k, v⟩ in t do ans := (k, v) :: ans return ans /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.toList /-- info: #[(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.toArray /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keys /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.keysArray /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.values /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)]).toList /-- info: Std.TreeMap.Raw.ofList [(1, 4)] -/ #guard_msgs in #eval TreeMap.Raw.ofList [(1, 2), (1, 4)] local instance : Inhabited ((_ : Nat) × Nat) where default := ⟨0, 0⟩ /-- info: some (2, 4) -/ #guard_msgs in #eval t.entryAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.entryAtIdx? 3 /-- info: (2, 4) -/ #guard_msgs in #eval t.entryAtIdx! 1 /-- info: (2, 4) -/ #guard_msgs in #eval t.entryAtIdxD 1 ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval t.entryAtIdxD 3 ⟨42, 3⟩ /-- info: some 2 -/ #guard_msgs in #eval t.keyAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.keyAtIdx? 3 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.keyAtIdxD 3 42 /-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getEntryLT! x /-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩ /-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x /-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getEntryLE! x /-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩ /-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getEntryGE! x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩ /-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getEntryGT! x /-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩ /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getKeyLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getKeyLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getKeyGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getKeyGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42 /-- info: some (1, 2) -/ #guard_msgs in #eval t.minEntry? /-- info: none -/ #guard_msgs in #eval (∅ : TreeMap.Raw Nat Nat).minEntry? /-- info: (1, 2) -/ #guard_msgs in #eval t.minEntry! /-- info: (1, 2) -/ #guard_msgs in #eval t.minEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval (∅ : TreeMap.Raw Nat Nat).minEntryD ⟨42, 3⟩ /-- info: some (3, 6) -/ #guard_msgs in #eval t.maxEntry? /-- info: none -/ #guard_msgs in #eval (∅ : TreeMap.Raw Nat Nat).maxEntry? /-- info: (3, 6) -/ #guard_msgs in #eval t.maxEntry! /-- info: (3, 6) -/ #guard_msgs in #eval t.maxEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval (∅ : TreeMap.Raw Nat Nat).maxEntryD ⟨42, 3⟩ /-- info: (Std.TreeMap.Raw.ofList [(3, 6)], Std.TreeMap.Raw.ofList [(1, 2), (2, 4)]) -/ #guard_msgs in #eval t.partition fun k v => k + 3 == v /-- info: (Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)], Std.TreeMap.Raw.ofList []) -/ #guard_msgs in #eval t.partition fun _ _ => true /-- info: (Std.TreeMap.Raw.ofList [], Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)]) -/ #guard_msgs in #eval t.partition fun _ _ => false /-- info: (Std.TreeMap.Raw.ofList [], Std.TreeMap.Raw.ofList []) -/ #guard_msgs in #eval (∅ : TreeMap.Raw Nat Nat).partition fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun k v => k + 5 == v /-- info: false -/ #guard_msgs in #eval t.all fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k v => k + k == v /-- info: false -/ #guard_msgs in #eval t.all fun k v => k + 3 == v /-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.TreeMap.Raw.ofList [(2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.TreeMap.Raw.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] /-- info: Std.TreeMap.Raw.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval TreeMap.Raw.mergeWith (fun _ v _ => v) t ∅ /-- info: Std.TreeMap.Raw.ofList [(0, 0), (1, 0), (2, 0), (3, 6)] -/ #guard_msgs in #eval TreeMap.Raw.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩]) /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keysIter.toList /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.valuesIter.toList /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t[*...*].toList /-- info: [(1, 2), (2, 4)] -/ #guard_msgs in #eval t[*...=2].toList /-- info: [(1, 2)] -/ #guard_msgs in #eval t[*...<2].toList /-- info: [(2, 4), (3, 6)] -/ #guard_msgs in #eval t[2...*].toList /-- info: [(2, 4), (3, 6)] -/ #guard_msgs in #eval t[2...=3].toList /-- info: [(2, 4)] -/ #guard_msgs in #eval t[2...<3].toList /-- info: [(2, 4), (3, 6)] -/ #guard_msgs in #eval t[1<...*].toList /-- info: [(2, 4), (3, 6)] -/ #guard_msgs in #eval t[1<...=3].toList /-- info: [(2, 4)] -/ #guard_msgs in #eval t[1<...<3].toList end TreeMap.Raw namespace TreeMap def t : TreeMap Nat Nat := .ofList [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] /-- info: [(2, 8)] -/ #guard_msgs in #eval (t.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [(1, none), (2, some 8), (3, none)] -/ #guard_msgs in #eval (t.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList /-- info: [(3, 6)] -/ #guard_msgs in #eval (t.filter fun _ v => v > 4).toList /-- info: [(3, 6), (2, 4), (1, 2)] -/ #guard_msgs in #eval Id.run do let mut ans : List (Nat × Nat) := [] for ⟨k, v⟩ in t do ans := (k, v) :: ans return ans /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.toList /-- info: #[(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.toArray /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keys /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.keysArray /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.values /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (TreeMap.ofList [(1, 2), (2, 4), (3, 6)]).toList /-- info: Std.TreeMap.ofList [(1, 4)] -/ #guard_msgs in #eval TreeMap.ofList [(1, 2), (1, 4)] local instance : Inhabited ((_ : Nat) × Nat) where default := ⟨0, 0⟩ /-- info: some (2, 4) -/ #guard_msgs in #eval t.entryAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.entryAtIdx? 3 /-- info: (2, 4) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.entryAtIdx 1 sorry /-- info: (2, 4) -/ #guard_msgs in #eval t.entryAtIdx! 1 /-- info: (2, 4) -/ #guard_msgs in #eval t.entryAtIdxD 1 ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval t.entryAtIdxD 3 ⟨42, 3⟩ /-- info: some 2 -/ #guard_msgs in #eval t.keyAtIdx? 1 /-- info: none -/ #guard_msgs in #eval t.keyAtIdx? 3 /-- info: 2 --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.keyAtIdx 1 sorry /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.keyAtIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.keyAtIdxD 3 42 /-- info: [none, none, some (1, 2), some (2, 4), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLT? x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getEntryLT! x /-- info: [(42, 3), (42, 3), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLTD x ⟨42, 3⟩ /-- info: [none, some (1, 2), some (2, 4), some (3, 6), some (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLE? x /-- info: [(1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getEntryLE! x /-- info: [(42, 3), (1, 2), (2, 4), (3, 6), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryLED x ⟨42, 3⟩ /-- info: [some (1, 2), some (1, 2), some (2, 4), some (3, 6), none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGE? x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getEntryGE! x /-- info: [(1, 2), (1, 2), (2, 4), (3, 6), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGED x ⟨42, 3⟩ /-- info: [some (1, 2), some (2, 4), some (3, 6), none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGT? x /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getEntryGT! x /-- info: [(1, 2), (2, 4), (3, 6), (42, 3), (42, 3)] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getEntryGTD x ⟨42, 3⟩ /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getKeyLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getKeyLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getKeyGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getKeyGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getKeyGTD x 42 /-- info: some (1, 2) -/ #guard_msgs in #eval t.minEntry? /-- info: (1, 2) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.minEntry sorry /-- info: none -/ #guard_msgs in #eval (∅ : TreeMap Nat Nat).minEntry? /-- info: (1, 2) -/ #guard_msgs in #eval t.minEntry! /-- info: (1, 2) -/ #guard_msgs in #eval t.minEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval (∅ : TreeMap Nat Nat).minEntryD ⟨42, 3⟩ /-- info: some (3, 6) -/ #guard_msgs in #eval t.maxEntry? /-- info: none -/ #guard_msgs in #eval (∅ : TreeMap Nat Nat).maxEntry? /-- info: (3, 6) --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.maxEntry sorry /-- info: (3, 6) -/ #guard_msgs in #eval t.maxEntry! /-- info: (3, 6) -/ #guard_msgs in #eval t.maxEntryD ⟨42, 3⟩ /-- info: (42, 3) -/ #guard_msgs in #eval (∅ : TreeMap Nat Nat).maxEntryD ⟨42, 3⟩ /-- info: (Std.TreeMap.ofList [(3, 6)], Std.TreeMap.ofList [(1, 2), (2, 4)]) -/ #guard_msgs in #eval t.partition fun k v => k + 3 == v /-- info: (Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)], Std.TreeMap.ofList []) -/ #guard_msgs in #eval t.partition fun _ _ => true /-- info: (Std.TreeMap.ofList [], Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)]) -/ #guard_msgs in #eval t.partition fun _ _ => false /-- info: (Std.TreeMap.ofList [], Std.TreeMap.ofList []) -/ #guard_msgs in #eval (∅ : TreeMap Nat Nat).partition fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k v => k + 3 == v /-- info: false -/ #guard_msgs in #eval t.any fun k v => k + 5 == v /-- info: false -/ #guard_msgs in #eval t.all fun _ _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k v => k + k == v /-- info: false -/ #guard_msgs in #eval t.all fun k v => k + 3 == v /-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.TreeMap.ofList [(2, 4), (3, 6)] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.TreeMap.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] /-- info: Std.TreeMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval TreeMap.mergeWith (fun _ v _ => v) t ∅ /-- info: Std.TreeMap.ofList [(0, 0), (1, 0), (2, 0), (3, 6)] -/ #guard_msgs in #eval TreeMap.mergeWith (fun _ v v' => v' - v) t (.ofList [⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 2⟩]) /-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.keysIter.toList /-- info: [2, 4, 6] -/ #guard_msgs in #eval t.valuesIter.toList end TreeMap namespace TreeSet.Raw def t : TreeSet.Raw Nat := .ofList [1, 2, 3] /-- info: [3] -/ #guard_msgs in #eval (t.filter fun k => k > 2).toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.toList /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.toArray /-- info: [1, 2, 3] -/ #guard_msgs in #eval (TreeSet.Raw.ofList [1, 2, 3]).toList /-- info: Std.TreeSet.Raw.ofList [1] -/ #guard_msgs in #eval TreeSet.Raw.ofList [1, 1] /-- info: some 2 -/ #guard_msgs in #eval t.atIdx? 1 /-- info: none -/ #guard_msgs in #eval t.atIdx? 3 /-- info: 2 -/ #guard_msgs in #eval t.atIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.atIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.atIdxD 3 42 /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGTD x 42 /-- info: (Std.TreeSet.Raw.ofList [3], Std.TreeSet.Raw.ofList [1, 2]) -/ #guard_msgs in #eval t.partition fun k => k == 3 /-- info: (Std.TreeSet.Raw.ofList [1, 2, 3], Std.TreeSet.Raw.ofList []) -/ #guard_msgs in #eval t.partition fun _ => true /-- info: (Std.TreeSet.Raw.ofList [], Std.TreeSet.Raw.ofList [1, 2, 3]) -/ #guard_msgs in #eval t.partition fun _ => false /-- info: (Std.TreeSet.Raw.ofList [], Std.TreeSet.Raw.ofList []) -/ #guard_msgs in #eval (∅ : TreeSet.Raw Nat).partition fun k => k == 3 /-- info: false -/ #guard_msgs in #eval t.any fun _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k => k == 3 /-- info: false -/ #guard_msgs in #eval t.any fun k => k == 5 /-- info: false -/ #guard_msgs in #eval t.all fun _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k => k < 6 /-- info: false -/ #guard_msgs in #eval t.all fun k => k == 3 /-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.TreeSet.Raw.ofList [2, 3] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.TreeSet.Raw.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] /-- info: Std.TreeSet.Raw.ofList [1, 2, 3] -/ #guard_msgs in #eval TreeSet.Raw.merge t ∅ /-- info: Std.TreeSet.Raw.ofList [0, 1, 2, 3] -/ #guard_msgs in #eval TreeSet.Raw.merge t (.ofList [0, 1, 2]) /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.iter.toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t[*...*].toList /-- info: [1, 2] -/ #guard_msgs in #eval t[*...=2].toList /-- info: [1] -/ #guard_msgs in #eval t[*...<2].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[2...*].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[2...=3].toList /-- info: [2] -/ #guard_msgs in #eval t[2...<3].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[1<...*].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[1<...=3].toList /-- info: [2] -/ #guard_msgs in #eval t[1<...<3].toList end TreeSet.Raw namespace TreeSet def t : TreeSet Nat := .ofList [1, 2, 3] /-- info: [3] -/ #guard_msgs in #eval (t.filter fun k => k > 2).toList /-- info: [1, 2, 3] -/ #guard_msgs in #eval t.toList /-- info: #[1, 2, 3] -/ #guard_msgs in #eval t.toArray /-- info: some 2 -/ #guard_msgs in #eval t.atIdx? 1 /-- info: none -/ #guard_msgs in #eval t.atIdx? 3 /-- info: 2 --- warning: declaration uses `sorry` -/ #guard_msgs in #eval! t.atIdx 1 sorry /-- info: 2 -/ #guard_msgs in #eval t.atIdx! 1 /-- info: 2 -/ #guard_msgs in #eval t.atIdxD 1 42 /-- info: 42 -/ #guard_msgs in #eval t.atIdxD 3 42 /-- info: [none, none, some 1, some 2, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [2, 3, 4].map fun x => t.getLT! x /-- info: [42, 42, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLTD x 42 /-- info: [none, some 1, some 2, some 3, some 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLE? x /-- info: [1, 2, 3, 3] -/ #guard_msgs in #eval [1, 2, 3, 4].map fun x => t.getLE! x /-- info: [42, 1, 2, 3, 3] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getLED x 42 /-- info: [some 1, some 1, some 2, some 3, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGE? x /-- info: [1, 1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2, 3].map fun x => t.getGE! x /-- info: [1, 1, 2, 3, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGED x 42 /-- info: [some 1, some 2, some 3, none, none] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGT? x /-- info: [1, 2, 3] -/ #guard_msgs in #eval [0, 1, 2].map fun x => t.getGT! x /-- info: [1, 2, 3, 42, 42] -/ #guard_msgs in #eval [0, 1, 2, 3, 4].map fun x => t.getGTD x 42 /-- info: (Std.TreeSet.ofList [3], Std.TreeSet.ofList [1, 2]) -/ #guard_msgs in #eval t.partition fun k => k == 3 /-- info: (Std.TreeSet.ofList [1, 2, 3], Std.TreeSet.ofList []) -/ #guard_msgs in #eval t.partition fun _ => true /-- info: (Std.TreeSet.ofList [], Std.TreeSet.ofList [1, 2, 3]) -/ #guard_msgs in #eval t.partition fun _ => false /-- info: (Std.TreeSet.ofList [], Std.TreeSet.ofList []) -/ #guard_msgs in #eval (∅ : TreeSet Nat).partition fun k => k == 3 /-- info: false -/ #guard_msgs in #eval t.any fun _ => false /-- info: true -/ #guard_msgs in #eval t.any fun _ => true /-- info: true -/ #guard_msgs in #eval t.any fun k => k == 3 /-- info: false -/ #guard_msgs in #eval t.any fun k => k == 5 /-- info: false -/ #guard_msgs in #eval t.all fun _ => false /-- info: true -/ #guard_msgs in #eval t.all fun _ => true /-- info: true -/ #guard_msgs in #eval t.all fun k => k < 6 /-- info: false -/ #guard_msgs in #eval t.all fun k => k == 3 /-- info: Std.TreeSet.ofList [1, 2, 3] -/ #guard_msgs in #eval t.eraseMany [] /-- info: Std.TreeSet.ofList [1, 2, 3] -/ #guard_msgs in #eval t.eraseMany [0] /-- info: Std.TreeSet.ofList [2, 3] -/ #guard_msgs in #eval t.eraseMany [1] /-- info: Std.TreeSet.ofList [] -/ #guard_msgs in #eval t.eraseMany [1, 2, 3] /-- info: Std.TreeSet.ofList [1, 2, 3] -/ #guard_msgs in #eval TreeSet.merge t ∅ /-- info: Std.TreeSet.ofList [0, 1, 2, 3] -/ #guard_msgs in #eval TreeSet.merge t (.ofList [0, 1, 2]) /-- info: [1, 2, 3] -/ #guard_msgs in #eval t[*...*].toList /-- info: [1, 2] -/ #guard_msgs in #eval t[*...=2].toList /-- info: [1] -/ #guard_msgs in #eval t[*...<2].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[2...*].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[2...=3].toList /-- info: [2] -/ #guard_msgs in #eval t[2...<3].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[1<...*].toList /-- info: [2, 3] -/ #guard_msgs in #eval t[1<...=3].toList /-- info: [2] -/ #guard_msgs in #eval t[1<...<3].toList end TreeSet