max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add LevelSet and PersistentLevelSet

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-05 13:26:25 -08:00
parent b0fd7ad264
commit abc8811498
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Lean/Level.lean
View file

@ -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