Joerl.idr

data Vect : (n: Nat) -> (elem : Type) -> Type where
  Empty : Vect 0 elem
  OneAnd : elem -> Vect n elem -> Vect (S n) elem

showString : Show elem => Vect n elem -> String
showString Empty = ""
showString (OneAnd x y) = show x ++ showString y

Show elem => Show (Vect n elem) where
  show = showString

length : Vect n a -> Nat
length {n} _ = n

empty : Vect Z Int
empty = Empty
one : Vect (S Z) Int
one = OneAnd 1 Empty

append : Vect m a -> Vect n a -> Vect (m + n) a
append Empty Empty = Empty
append Empty v@(OneAnd x y) = v
append v@(OneAnd x z) Empty = OneAnd x (append z Empty)
append v@(OneAnd x z) (OneAnd y w) = OneAnd y (append z (OneAnd y w))

main : IO ()
main = print (append empty empty)