From abc8811498c71a36743607312dd94caea839f97c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2020 13:26:25 -0800 Subject: [PATCH] feat: add `LevelSet` and `PersistentLevelSet` --- src/Init/Lean/Level.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Lean/Level.lean b/src/Init/Lean/Level.lean index 262aab7309..447f6d2bfd 100644 --- a/src/Init/Lean/Level.lean +++ b/src/Init/Lean/Level.lean @@ -7,6 +7,8 @@ prelude import Init.Data.Option.Basic import Init.Data.HashMap import Init.Data.PersistentHashMap +import Init.Data.HashSet +import Init.Data.PersistentHashSet import Init.Lean.Data.Name import Init.Lean.Data.Format @@ -432,6 +434,9 @@ end Level abbrev LevelMap (α : Type) := HashMap Level α abbrev PersistentLevelMap (α : Type) := PHashMap Level α +abbrev LevelSet := HashSet Level +abbrev PersistentLevelSet := PHashSet Level +abbrev PLevelSet := PersistentLevelSet end Lean