on bf4e535 help sign in
Idris-dev/test/interactive003/interactive003.idr
10 lines 267 B history raw
1import Data.Vect
3app : Vect n a -> Vect m a -> Vect (n + m) a
4app [] ys = ?app_rhs_1
5app (x :: xs) ys = ?app_rhs_2
6
7vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
8vzipWith f [] [] = ?vzipWith_rhs_3
9vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_1