idris-1.3.0: test/regression002/reg002.idr

append : List a -> List a -> List a
append [] ys = ys
append (X :: XS) ys = X :: append XS ys