git.iko.soy/Idris-dev
on master help sign in
Small error message fix
81f2c89Edwin Brady
lib/prelude/vect.idr+2−2
compare with master
unifiedsplit
@@ -8,8 +8,8 @@ import prelude.fin
8infixr 10 ::
8infixr 10 ::
9
9
10data Vect : Set -> Nat -> Set where
10data Vect : Set -> Nat -> Set where
11− Nil : Vect a O
11+ Nil : Vect a 0
12− (::) : a -> Vect a k -> Vect a (S k)
12+ (::) : a -> Vect a k -> Vect a (1 + k)
13
13
14tail : Vect a (S n) -> Vect a n
14tail : Vect a (S n) -> Vect a n
15tail (x :: xs) = xs
15tail (x :: xs) = xs
src/Core/Elaborate.hs+7−1
@@ -286,7 +286,13 @@ prepare_apply fn imps =
286 when i (movelast n)
286 when i (movelast n)
287 mkClaims sc' is (n : claims)
287 mkClaims sc' is (n : claims)
288 mkClaims t [] claims = return (reverse claims)
288 mkClaims t [] claims = return (reverse claims)
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
289− mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
295+ | otherwise = fail $ "Too many arguments for " ++ show fn
290
296
291 doClaim ((i, _), n, t) = do claim n t
297 doClaim ((i, _), n, t) = do claim n t
292 when i (movelast n)
298 when i (movelast n)