------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4