Juvix.Builtin.V1.Nat.Base
Contents
builtin nat type NatSource#
Inductive natural numbers. I.e. whole non-negative numbers.
Constructors
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.
