Function types

[timbeurskens]

Support the ability to write relations as function applications:
A function can be described by means of a look-up table, such that the output of a function only depends on its inputs: f(a) = b.
This function type can be used to describe more complex operations, such as addition, multiplication, or prime factorization.

[timbeurskens]

Definitions:

• A function without arguments, equals a collection of variables:
• A function with n arguments and a single output can be expressed as a single proposition.
• A function with n outputs can be expressed as n functions with 1 output