{-# OPTIONS --cubical --safe #-}
module Cubical.Data.List.Base where

open import Agda.Builtin.List        public
open import Cubical.Core.Everything
open import Cubical.Data.Nat

module _ {ℓ} {A : Type ℓ} where

  infixr  _++_ _∷ʳ_

  [_] : A → List A
  [ a ] = a ∷ []

  _++_ : List A → List A → List A
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ xs ++ ys

  rev : List A → List A
  rev [] = []
  rev (x ∷ xs) = rev xs ++ [ x ]

  _∷ʳ_ : List A → A → List A
  xs ∷ʳ x = xs ++ x ∷ []

  length : List A → ℕ
  length [] = 
  length (x ∷ l) =  + length l