lean4-htt/src/Std/Data/ExtTreeSet.lean
Rob23oba 9bf5fc2fd3
feat: extensional tree maps (#8721)
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.
2025-06-26 13:13:45 +00:00

8 lines
223 B
Text

/-
Copyright (c) 2025 Robin Arnez. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robin Arnez
-/
prelude
import Std.Data.ExtTreeSet.Basic
import Std.Data.ExtTreeSet.Lemmas