3c46202 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+1−1

@@ -90,7 +90,7 @@ trace_malloc x = x -- compiled specially

90||| x (which is typically a pattern argument)

91||| @ x the larger value (typically a pattern argument)

92||| @ y the smaller value (typically an argument to a recursive call)

93−assert_smaller : (x, y : a) -> a

93+assert_smaller : (x : a) -> (y : b) -> b

94assert_smaller x y = y

95

96||| Assert to the totality checker than the given expression will always

src/IRTS/Compiler.hs+1−1

@@ -221,7 +221,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

221 | l == txt "Force"

222 -> LForce <$> irTerm vs env arg

223

224− (P _ (UN a) _, [_, _, arg])

224+ (P _ (UN a) _, [_, _, _, arg])

225 | a == txt "assert_smaller"

226 -> irTerm vs env arg

227

src/Idris/Coverage.hs+1−1

@@ -517,7 +517,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

517 -- find which argument in pargs <a> is smaller than, if any

518 checkSize a (p : ps) i

519 | a == p = Just (i, Same)

520− | (P _ (UN as) _, [_,arg,_]) <- unApply a,

520+ | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,

521 as == txt "assert_smaller" && arg == p

522 = Just (i, Smaller)

523 | smaller Nothing a (p, Nothing) = Just (i, Smaller)