Naturals

手工定义的自然数类型，加法对第一个参数递归。本模块用于演示渲染框架，并非数学开发的一部分。

The type

Nat 是常规的归纳类型，带有两个构造子 zero 与 suc。

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

open import Cubical.Foundations.Prelude

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

Addition

加法 _+_ 对第一个参数递归，故 $0 + m = m$ 与 $(1 + n) + m = 1 + (n + m)$ 在定义上成立。

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