module Prim.Data.Nat where
Primitive: Natural numbers🔗
The natural numbers are the initial type generated by a point and an endomorphism.
data Nat : Type where zero : Nat suc : Nat → Nat {-# BUILTIN NATURAL Nat #-}
Optimised functions on Nat🔗
The following functions on the natural numbers can be bound as BUILTINs to be replaced by native
versions operating directly on machine integers whenever possible.
infix 4 _==_ _<_ _≤_ infixl 8 _+_ _-_ infixl 9 _*_ _+_ : Nat → Nat → Nat zero + m = m suc n + m = suc (n + m) {-# BUILTIN NATPLUS _+_ #-} _-_ : Nat → Nat → Nat n - zero = n zero - suc m = zero suc n - suc m = n - m {-# BUILTIN NATMINUS _-_ #-} _*_ : Nat → Nat → Nat zero * m = zero suc n * m = m + n * m {-# BUILTIN NATTIMES _*_ #-} _==_ : Nat → Nat → Bool zero == zero = true suc n == suc m = n == m _ == _ = false {-# BUILTIN NATEQUALS _==_ #-} _<_ : Nat → Nat → Bool _ < zero = false zero < suc _ = true suc n < suc m = n < m {-# BUILTIN NATLESS _<_ #-} _≤_ : Nat → Nat → Bool x ≤ y = x < suc y {-# INLINE _≤_ #-}