refsIn should take all the Ps
Ps are references, after all, and if they're under a lambda they refer
to something else.
commit8628481b7a8216ed1e5b6de9623b5b86250e0233
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 1 Jan 2015, 16:53 (12 years ago)
parentd75ff02
src/Idris/Core/TT.hs+1−1
@@ -1416,7 +1416,7 @@ orderPats tm = op [] tm
14161416
14171417refsIn :: TT Name -> [Name]
14181418refsIn (P _ n _) = [n]
1419−refsIn (Bind n b t) = nub $ nb b ++ (refsIn t \\ [n])
1419+refsIn (Bind n b t) = nub $ nb b ++ refsIn t
14201420 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
14211421 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
14221422 nb t = refsIn (binderTy t)