9bf5fc2fd3
This PR adds the types `Std.ExtDTreeMap`, `Std.ExtTreeMap` and `Std.ExtTreeSet` of extensional tree maps and sets. These are very similar in construction to the existing extensional hash maps with one exception: extensional tree maps and sets provide all functions from regular tree maps and sets. This is possible because in contrast to hash maps, tree maps are always ordered.
30 lines
895 B
Text
30 lines
895 B
Text
/-
|
|
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Markus Himmel
|
|
-/
|
|
prelude
|
|
import Std.Data.DHashMap
|
|
import Std.Data.HashMap
|
|
import Std.Data.HashSet
|
|
import Std.Data.DTreeMap
|
|
import Std.Data.TreeMap
|
|
import Std.Data.TreeSet
|
|
import Std.Data.ExtDHashMap
|
|
import Std.Data.ExtHashMap
|
|
import Std.Data.ExtHashSet
|
|
import Std.Data.ExtDTreeMap
|
|
import Std.Data.ExtTreeMap
|
|
import Std.Data.ExtTreeSet
|
|
|
|
-- The imports above only import the modules needed to work with the version which bundles
|
|
-- the well-formedness invariant, so we need to additionally import the files that deal with the
|
|
-- unbundled version
|
|
import Std.Data.DHashMap.RawLemmas
|
|
import Std.Data.HashMap.RawLemmas
|
|
import Std.Data.HashSet.RawLemmas
|
|
import Std.Data.DTreeMap.Raw
|
|
import Std.Data.TreeMap.Raw
|
|
import Std.Data.TreeSet.Raw
|
|
|
|
import Std.Data.Iterators
|