0f1133fe69
This PR introduces ordered map data structures, namely `DTreeMap`, `TreeMap`, `TreeSet` and their `.Raw` variants, into the standard library. There are still some operations missing that the hash map has. As of now, the operations are unverified, but the corresponding lemmas will follow in subsequent PRs. While the tree map has already been optimized, more micro-optimization will follow as soon as the new code generator is ready. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
19 lines
625 B
Text
19 lines
625 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
|
|
|
|
-- The three 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
|