on 54e4e41 help sign in
Idris-dev/test/interactive004/interactive004.idr
9 lines 208 B history raw
1import Data.Vect
3foo : Nat -> Nat -> Nat
4foo k j = ?foo_rhs1
6append : (n : Nat) -> (m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
7append Z m [] ys = ys
8append (S k) m (x :: xs) ys = x :: ?append_rhs1