Doubling

Doubling, defined via addition. This module exists to demonstrate cross-module hyperlinks, inline references, and math in the rendering framework.

Definition

Here _+_ is the addition from the previous module, so double adds a number to itself.

{-# 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

By definition, doubling satisfies $\mathrm{double}(n) = n + n$.