Module math

Function types relating to church numerals and mathematics.

The const-numeral feature flag, off by default, adds a wrapper to allow converting any church numeral to a number. This flag requires #![feature(generic_const_exprs)].

Structs

Add

Adds two church numerals.

ConstIncrement

Increments a ConstNumber by one. Used to define ToNumber.

ConstNumber

Constant number returned by converting a church numeral.

Eq

Returns whether two numbers are equal.

Exponent

Raises a numeral to the power of another.

IsZero

Returns whether a number is zero.

Leq

Returns whether one number is less than or equal to another.

Multiply

Multiplies two church numerals - this is simply composition.

Predecessor

Predecessor function. Gets the number below a given church numeral.

Subtract

Subtracts two church numerals.

Successor

Successor function. Returns a number plus one.

ToNumber

Converts a church numeral to a constant number. See ConstNumber.

Type Aliases

Zero

Church numeral for zero.