------------------------------------------------------------------------
-- Coinductive "natural" numbers
------------------------------------------------------------------------

module Data.Conat where

open import Coinduction
open import Data.Nat using (; zero; suc)

------------------------------------------------------------------------
-- The type

data Coℕ : Set where
  zero : Coℕ
  suc  : (n :  Coℕ)  Coℕ

------------------------------------------------------------------------
-- Some operations

fromℕ :   Coℕ
fromℕ zero    = zero
fromℕ (suc n) = suc ( fromℕ n)

∞ℕ : Coℕ
∞ℕ = suc ( ∞ℕ)

infixl 6 _+_

_+_ : Coℕ  Coℕ  Coℕ
zero  + n = n
suc m + n = suc ( ( m + n))