@@ -486,7 +486,7 @@ intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)
486486intTyName (ITChar) = "Char"
487487intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count
488488
489−data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors
489+data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
490490 deriving (Show, Eq, Ord)
491491{-!
492492deriving instance NFData IntTy
@@ -792,7 +792,7 @@ instance TermSize (TT Name) where
792792 | otherwise = 1
793793 termsize n (V _) = 1
794794 -- for `Bind` terms, we can erroneously declare a term
795− -- "recursive => really big" if the name of the bound
795+ -- "recursive => really big" if the name of the bound
796796 -- variable is the same as the name we're using
797797 -- So generate a different name in that case.
798798 termsize n (Bind n' (Let t v) sc)
@@ -971,19 +971,19 @@ subst n v tm = fst $ subst' 0 tm
971971 subst' i t@(Bind x b sc) | x /= n
972972 = let (b', ub) = substB' i b
973973 (sc', usc) = subst' (i+1) sc in
974− if ub || usc then (Bind x b' sc', True) else (t, False)
975− subst' i t@(App f a) = let (f', uf) = subst' i f
974+ if ub || usc then (Bind x b' sc', True) else (t, False)
975+ subst' i t@(App f a) = let (f', uf) = subst' i f
976976 (a', ua) = subst' i a in
977977 if uf || ua then (App f' a', True) else (t, False)
978978 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
979979 if u then (Proj x' idx, u) else (t, False)
980980 subst' i t = (t, False)
981981
982− substB' i b@(Let t v) = let (t', ut) = subst' i t
982+ substB' i b@(Let t v) = let (t', ut) = subst' i t
983983 (v', uv) = subst' i v in
984984 if ut || uv then (Let t' v', True)
985985 else (b, False)
986− substB' i b@(Guess t v) = let (t', ut) = subst' i t
986+ substB' i b@(Guess t v) = let (t', ut) = subst' i t
987987 (v', uv) = subst' i v in
988988 if ut || uv then (Guess t' v', True)
989989 else (b, False)
@@ -1090,7 +1090,7 @@ unList tm = case unApply tm of
10901090-- Bruijn indices.
10911091forget :: TT Name -> Raw
10921092forget tm = forgetEnv [] tm
1093−
1093+
10941094forgetEnv :: [Name] -> TT Name -> Raw
10951095forgetEnv env (P _ n _) = Var n
10961096forgetEnv env (V i) = Var (env !! i)
@@ -1384,7 +1384,7 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in
13841384 orderPats $ bindPats (reverse ps) tm'
13851385 where
13861386 bindPats [] tm = tm
1387− bindPats ((n, t):ps) tm
1387+ bindPats ((n, t):ps) tm
13881388 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
13891389 | otherwise = bindPats ps tm
13901390