UniAgda.Core.Types.Nat

Table of Contents

1 Prelude

2 The Natural Numbers

The natural numbers are defined inductively by zero and the successor function.

data   : Type lzero where
  zero : 
  suc :  -> 
{-# BUILTIN NATURAL  #-}

3 Addition, subtraction, multiplication and exponentiation

Author: James Leslie

Created: 2021-03-27 Sat 10:47