4
open import Common.Prelude using (Nat; zero; suc)
6
module _ {a} (A : Set a) where
8
data List : Set a where
10
_∷_ : (x : A) (xs : List) → List
12
module _ {a} {A : Set a} where
14
_++_ : List → List → List
16
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
20
test = (5 ∷ []) ++ (3 ∷ [])