A term definition has the form`f p_1 p_2 … p_n = e`

where`f`

is the name of the term being defined. The parameters`p_1`

through`p_n`

are the names of parameters, if any (if the term is a function), separated by spaces. The right-hand side of the`=`

sign is anyUnison expression.

The names of the parameters as well as the name of the term are bound as local variables in the expression on the right-hand side (also known as thebodyof the function). When the function is called, the parameter names are bound to any arguments passed in the call. Seefunction applicationfor details on the call semantics of functions.

If the term takes no arguments, the term has the value of the fully evaluated expression on the right-hand side and is not a function.

The expression comprising the right-hand side can refer to the name given to the definition in the left-hand side. In that case, it’s a recursive definition. For example:

The above defines a function`sumUpTo`

that recursively sums all the natural numbers less than some number`n`

.As an example,`sumUpTo 3`

is`1 + 2 + 3`

,which is`6`

.

Note: The expression`n Nat.- 1`

on line 4 above subtracts`1`

from the natural number`n`

.Since the natural numbers are not closed under subtraction (''n Nat.subtractInt 1'' is an`Int`

),we use the operation`-`

which has the convention that`0 Nat.- n Nat.== 0`

for all natural numbers`n`

.Unison's type system saves us from having to deal with negative numbers here.