From 1ae21864844d739aace338bd3852833103244fbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 11 Aug 2019 15:48:27 -0700
Subject: [PATCH] fix(library/init/lean/elaborator/alias): avoid duplicates

---
 library/init/lean/elaborator/alias.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/elaborator/alias.lean b/library/init/lean/elaborator/alias.lean
index 620e83746a..65e61fa10f 100644
--- a/library/init/lean/elaborator/alias.lean
+++ b/library/init/lean/elaborator/alias.lean
@@ -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