Functions of several arguments

Uses Functions, Tuples

Functions of more than one argument are defined as functions of a single tuple argument.

Function application can be written without the explicit creation of a tuple:
 arg1:𝕊, arg2:𝕊, ((arg1, arg2) → (value:𝕊))[arg1, arg2] : value
 arg1:𝕊, arg2:𝕊, arg3:𝕊, ((arg1, arg2, arg3) → (value:𝕊))[arg1, arg2, arg3] : value

Example

Uses _example Integers

The greatest common divisor of two natural numbers is defined as
 _example gcd : (ℕ, ℕ) → ℕ

It can be computed using Euclid's algorithm, which considers three cases:

1. The two numbers are equal:
 _example gcd[1]: n:ℕ, gcd[n, n] ⇒ n

2. The first number is larger:
 _example gcd[2]: n:ℕ, m:ℕ, gcd[n, m] ⇒ gcd[n - m, m] | n > m

3. The second number is larger:
 _example gcd[3]: n:ℕ, m:ℕ, gcd[n, m] ⇒ gcd[n, m - n]

Applications:
 _example gcd[2, 3] ⇒ 1
 _example gcd[3, 2] ⇒ 1
 _example gcd[42, 7] ⇒ 7