------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists defined in terms of the reflexive-transitive closure, Star
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Star.List where

open import Data.Star.Nat using (; _+_; zero)
open import Data.Unit.Base using (tt)
open import Relation.Binary.Construct.Always using (Always)
open import Relation.Binary.Construct.Constant using (Const)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_; fold)

-- Lists.

List :  {a}  Set a  Set a
List A = Star (Const A) tt tt

-- Nil and cons.

[] :  {a} {A : Set a}  List A
[] = ε

infixr 5 _∷_

_∷_ :  {a} {A : Set a}  A  List A  List A
_∷_ = _◅_

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

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