git.iko.soy/Idris-dev
on master help sign in
Small error message fix
commit81f2c893f9e2368fb2c62652ed13b81f76a7690d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 7 Feb 2012, 12:33 (15 years ago) parent4bcfa68
2 files changed+9−3
compare with master
unifiedsplit
lib/prelude/vect.idr+2−2 src/Core/Elaborate.hs+7−1
lib/prelude/vect.idr+2−2
@@ -8,8 +8,8 @@ import prelude.fin
88infixr 10 ::
99
1010data Vect : Set -> Nat -> Set where
11− Nil : Vect a O
12− (::) : a -> Vect a k -> Vect a (S k)
11+ Nil : Vect a 0
12+ (::) : a -> Vect a k -> Vect a (1 + k)
1313
1414tail : Vect a (S n) -> Vect a n
1515tail (x :: xs) = xs
src/Core/Elaborate.hs+7−1
@@ -286,7 +286,13 @@ prepare_apply fn imps =
286286 when i (movelast n)
287287 mkClaims sc' is (n : claims)
288288 mkClaims t [] claims = return (reverse claims)
289− mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
289+ mkClaims _ _ _
290+ | Var n <- fn
291+ = do ctxt <- get_context
292+ case lookupTy Nothing n ctxt of
293+ [] -> lift $ tfail $ NoSuchVariable n
294+ _ -> fail $ "Too many arguments for " ++ show fn
295+ | otherwise = fail $ "Too many arguments for " ++ show fn
290296
291297 doClaim ((i, _), n, t) = do claim n t
292298 when i (movelast n)