BoundedNat.agda

module BoundedNat where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

record BoundedNat (min max : ℕ) : Set where
  constructor mk
  field
    val : ℕ
    property : (min ≤ val) × (val ≤ max)

add : ∀ {min1 max1 min2 max2} → BoundedNat min1 max1 → BoundedNat min2 max2 → BoundedNat (min1 + min2) (max1 + max2)
add (mk a (aleft , aright)) (mk b (bleft , bright)) = mk (a + b) (+-mono-≤ aleft bleft , +-mono-≤ aright bright)

a : BoundedNat 0 2
a = mk 1 (z≤n , s≤s z≤n)

b : BoundedNat 1 3
b = mk 2 (s≤s z≤n , s≤s (s≤s z≤n))

sum = add a b
-- Compute normal form with: C-c C-n
-- > `mk 3 (s≤s z≤n , s≤s (s≤s (s≤s z≤n)))`
-- Infer simplified type with: C-c C-d
-- > `BoundedNat 1 5`