git.iko.soy/Idris-dev
on 33166ee help sign in
Idris-dev/samples/tutorial/vbroken.idr
10 lines 228 B history raw
1module Vect
3data Vect : Nat -> Type -> Type where
4 Nil : Vect Z a
5 (::) : a -> Vect k a -> Vect (S k) a
7(++) : Vect n a -> Vect m a -> Vect (n + m) a
8(++) Nil ys = ys
9(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN