Stdlib.Data.Nat

Contents

builtin nat type NatSource #

Inductive natural numbers. I.e. whole non-negative numbers.

Constructors

\| zero : Nat
\| suc : Nat → Nat

builtin nat-plus + : Nat → Nat → NatSource #

Addition for Nats.

builtin nat-mul * : Nat → Nat → NatSource #

Multiplication for Nats.

builtin nat-sub sub : Nat → Nat → NatSource #

Truncated subtraction for Nats.

builtin nat-udiv terminating udiv : Nat → Nat → NatSource #

Division for Nats. Returns zero if the first element is zero.

builtin nat-div div : Nat → Nat → NatSource #

Division for Nats.

builtin nat-mod mod : Nat → Nat → NatSource #

Modulo for Nats.

builtin nat-to-string axiom natToString : Nat -> StringSource #

Converts a Nat into a String.

builtin string-to-nat axiom stringToNat : String -> NatSource #

Partial function that converts a String into a Nat.

Description

Definitions