Natural Numbers
Table of Contents
1 Natural numbers
module Lib.Data.Nat where
The standard library provides the usual inductive definition of natural numbers using unary encoding. This file gives the induction principle of Nat together with some shortcuts.
import Stdlib.Nat.Base
1.1 Induction principle
ind-Nat (P : Nat → U) (pz : P zero) (ps : ((n : Nat) → P n → P (suc n))) : (n : Nat) → P n = split zero → pz suc n' → ps n' (ind-Nat P pz ps n')
1.2 Shortcuts
one-Nat : Nat = suc zero two-Nat : Nat = suc one-Nat three-Nat : Nat = suc two-Nat four-Nat : Nat = suc three-Nat five-Nat : Nat = suc four-Nat six-Nat : Nat = suc five-Nat seven-Nat : Nat = suc six-Nat eight-Nat : Nat = suc seven-Nat nine-Nat : Nat = suc eight-Nat ten-Nat : Nat = suc nine-Nat
1.3 Functions
The addition is trivially defined by induction.
plus-Nat (m : Nat) : Nat → Nat = split zero → m suc k → suc (plus-Nat m k)
The multiplication is defined using addition.
times-Nat (m : Nat) : Nat → Nat = split zero → zero suc k → plus-Nat m (times-Nat k m)