Doubling

通过加法定义的加倍。本模块用于演示渲染框架中的跨模块超链接、行内引用与数学公式。

Definition

此处 _+_ 是上一模块中的加法，故 double 将一个数与其自身相加。

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

open import Cubical.Foundations.Prelude
open import Example.Naturals

double : Nat → Nat
double n = n + n

A property

根据定义，加倍满足 $\mathrm{double}(n) = n + n$。