nspec - 0.1.3

Juvix.Builtin.V1.Nat.Base

Definitions

builtin nat type NatSource#

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

Constructors

| zero
| suc 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 (n m : Nat) : NatSource#

Division for Nats.

builtin nat-mod mod (n m : Nat) : NatSource#

Modulo for Nats.