------------------------------------------------------------------------
-- Natural numbers with fast addition (for use together with
-- DifferenceVec)
------------------------------------------------------------------------

module Data.DifferenceNat where

open import Data.Nat as N using ()
open import Function

infixl 6 _+_

Diffℕ : Set
Diffℕ =   

0# : Diffℕ
0# = λ k  k

suc : Diffℕ  Diffℕ
suc n = λ k  N.suc (n k)

1# : Diffℕ
1# = suc 0#

_+_ : Diffℕ  Diffℕ  Diffℕ
m + n = λ k  m (n k)

toℕ : Diffℕ  
toℕ n = n 0

-- fromℕ n is linear in the size of n.

fromℕ :   Diffℕ
fromℕ n = λ k  n  N._+_  k