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

fix(library/init/lean/elaborator/alias): avoid duplicates

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-11 15:48:27 -07:00
parent 3dad81daee
commit 1ae2186484
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/elaborator/alias.lean
View file

@ -15,8 +15,8 @@ abbrev AliasEntry := Name × Name
def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
match s.find e.1 with
| none => s.insert e.1 [e.2]
| some ids => s.insert e.1 (e.2 :: ids)
| none => s.insert e.1 [e.2]
| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
def mkAliasExtension : IO (SimplePersistentEnvExtension AliasEntry AliasState) :=
registerSimplePersistentEnvExtension {
@ -35,6 +35,6 @@ aliasExtension.addEntry env (a, e)
def getAliases (env : Environment) (a : Name) : List Name :=
match (aliasExtension.getState env).find a with
| none => []
| some as => as
| some es => es
end Lean