split-in-box.gr rewrite test error #313
Description
Input:
data N (n : Nat) where
Z : N 0;
S : forall {n : Nat}. (m : N n) -> N (n+1)
data Vec (n : Nat) (a : Type) where
Nil : Vec 0 a;
Cons : forall {n : Nat} . a -> Vec n a -> Vec (n+1) a
take : forall {a : Type, n : Nat, k : Nat} . N k -> (Vec (n+k) a) [0..1] -> Vec k a
take Z [vec] = ?;
take (S m0) [vec] = {! m0 vec !}
Expected:
...
take : forall {a : Type, n : Nat, k : Nat} . N k -> (Vec (n+k) a) [0..1] -> Vec k a
take Z [vec] = ?;
take (S Z) [(Cons vec0 vec1)] = ?;
take (S (S m0)) [(Cons vec0 vec1)] = ?
Actual:
...
take : forall {a : Type, n : Nat, k : Nat} . N k -> (Vec (n+k) a) [0..1] -> Vec k a
take Z [vec] = ?;
take (S Z) [Nil] = ?;
take (S Z) [(Cons vec0 vec1)] = ?;
take (S (S m0)) [Nil] = ?;
take (S (S m0)) [(Cons vec0 vec1)] = ?