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

module Data.Star.Nat where

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

-- 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#