git.iko.soy/Idris-dev
on master help sign in
Modified uniqueBinders function to prevent overlapping binders.
a2028e1bmsherman
src/Idris/Core/TT.hs+3−2
compare with master
unifiedsplit
@@ -1056,8 +1056,9 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
1056
1056
1057uniqueBinders :: [Name] -> TT Name -> TT Name
1057uniqueBinders :: [Name] -> TT Name -> TT Name
1058uniqueBinders ns (Bind n b sc)
1058uniqueBinders ns (Bind n b sc)
1059− = let n' = uniqueName n ns in
1059+ = let n' = uniqueName n ns
1060+ ns' = n' : ns in
1060− Bind n' (fmap (uniqueBinders (n':ns)) b) (uniqueBinders ns sc)
1061+ Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)
1061uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)
1062uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)
1062uniqueBinders ns t = t
1063uniqueBinders ns t = t
1063
1064