------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers defined using the reflexive-transitive closure, Star
------------------------------------------------------------------------

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

module Data.Star.Nat where

open import Data.Unit.Base using (tt)
open import Function.Base using (const)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Always using (Always)

-- Natural numbers.

 : Set
 = Star Always tt tt

-- Zero and successor.

zero : 
zero = ε

suc :   
suc = _◅_ _

-- The length of a star-list.

length :  {i t} {I : Set i} {T : Rel I t} {i j}  Star T i j  
length = gmap (const _) (const _)

-- Arithmetic.

infixl 7 _*_
infixl 6 _+_ _∸_

_+_ :     
_+_ = _◅◅_

_*_ :     
_*_ m = const m 

_∸_ :     
m        ε       = m
ε        (_  n) = zero
(_  m)  (_  n) = m  n

-- Some constants.

0# = zero
1# = suc 0#
2# = suc 1#
3# = suc 2#
4# = suc 3#
5# = suc 4#