{-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.Data.List.Base where open import Agda.Builtin.List public open import Cubical.Core.Everything open import Cubical.Data.Maybe open import Cubical.Data.Nat module _ {ℓ} {A : Type ℓ} where infixr 5 _++_ infixl 5 _∷ʳ_ [_] : 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 [] = 0 length (x ∷ l) = 1 + length l map : ∀ {ℓ'} {B : Type ℓ'} → (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = f x ∷ map f xs map2 : ∀ {ℓ' ℓ''} {B : Type ℓ'} {C : Type ℓ''} → (A → B → C) → List A → List B → List C map2 f [] _ = [] map2 f _ [] = [] map2 f (x ∷ xs) (y ∷ ys) = f x y ∷ map2 f xs ys foldr : ∀ {ℓ'} {B : Type ℓ'} → (A → B → B) → B → List A → B foldr f b [] = b foldr f b (x ∷ xs) = f x (foldr f b xs) foldl : ∀ {ℓ'} {B : Type ℓ'} → (B → A → B) → B → List A → B foldl f b [] = b foldl f b (x ∷ xs) = foldl f (f b x) xs