------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.List where

open import Data.Star
open import Data.Unit
open import Relation.Binary.Simple
open import Data.Star.Nat

-- Lists.

List : Set → Set
List a = Star (Const a) tt tt

-- Nil and cons.

[] : ∀ {a} → List a
[] = ε

infixr 5 _∷_

_∷_ : ∀ {a} → a → List a → List a
_∷_ = _◅_

-- The sum of the elements in a list containing natural numbers.

sum : List ℕ → ℕ
sum = fold (Star Always) _+_ zero