a2028e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Modified uniqueBinders function to prevent overlapping binders.

commita2028e131973f4410ace04d5e75af805288aeb06 authorbmsherman <bmsherman@users.noreply.github.com> dateMon 26 May 2014, 17:50 (12 years ago) parentd61641d

1 file changed+3−2

compare with master

unifiedsplit

src/Idris/Core/TT.hs+3−2

src/Idris/Core/TT.hs+3−2

@@ -1056,8 +1056,9 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

10561056

10571057uniqueBinders :: [Name] -> TT Name -> TT Name

10581058uniqueBinders ns (Bind n b sc)

1059− = let n' = uniqueName n ns in

1060− Bind n' (fmap (uniqueBinders (n':ns)) b) (uniqueBinders ns sc)

1059+ = let n' = uniqueName n ns

1060+ ns' = n' : ns in

1061+ Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)

10611062uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

10621063uniqueBinders ns t = t

10631064