Naturals

A hand-rolled type of natural numbers, with addition by recursion on the first argument. This module exists to demonstrate the rendering framework; it is not part of the mathematical development.

The type

Nat is the usual inductive type with two constructors, zero and

suc.

{-# OPTIONS --cubical --safe --guardedness #-}
module Example.Naturals where

open import Cubical.Foundations.Prelude

data Nat : Type where
  zero : Nat
  suc  : Nat → Nat

Addition

Addition _+_ recurses on the first argument, so that $0 + m = m$ and

$(1 + n) + m = 1 + (n + m)$ hold definitionally.

_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)