Juvix.Builtin.V1.Nat.Base

Contents

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.

Description

Definitions