on 7afa310 help sign in
Idris-dev/test/interactive004/interactive004.idr
7 lines 190 B history raw
1foo : Nat -> Nat -> Nat
2foo k j = ?foo_rhs1
4append : (n : Nat) -> (m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
5append Z m [] ys = ys
6append (S k) m (x :: xs) ys = x :: ?append_rhs1