| | | A.2.7 Function Values and Applications |
LAMBDA(I1:T1, I2:T2, ...,
In:Tn): E
E(E1, ..., En)
The function value expression
LAMBDA(I1:T1, I2:T2, ..., In:Tn): E
denotes the function that, given arguments I1 of type T1, I2 of type T2, ..., In of type Tn, returns the value of expression E (in which I1, I2, ..., In may freely occur). Correspondingly the type of the expression is the function type (T1, T2, ..., Tn) -> T where T is the type of E.
The function application expression E(E1, ..., En) consists of an expression E denoting a value of type (T1, T2, ..., Tn) -> T for some types T1, T2, ..., Tn, T and of expressions E1 of type T1, E2 of type T2, ..., En of type Tn. The value of the application is the result of E when applied to the values of E1, E2, ..., En; the type of the application is T.
In a function value expression, for multiple parameters with the same type, the parameter type needs to be declared only once, thus it is for example legal to write
LAMBDA(x,y:NAT, z:REAL): x*y+z
| | | A.2.7 Function Values and Applications |