timesTwo : Nat -> Nat
timesTwo x = x * 2
The first line in the above is atype signature.The type signature
timesTwo : Nat -> Natdeclares that the term named
timesTwois a function accepting an argument of type
Natand computes a value of type
Natis the type of 64-bit natural numbers starting from zero. SeeUnison typesfor details.
The second line is the term definition. The
=sign splits the definition into aleft-hand side,which is the term being defined, and theright-hand side,which is the definition of the term.
The general form of a term binding is:
name : Type
name p_1 p_2 … p_n = expression