Go backward to
Proof of Correspondence
Go up to
Top
Go forward to
Typing of Parameter Lists
Parameter Lists
Bind multiple values to multiple names.
define
I(I
1
:
theta
1
, I
2
:
theta
2
, ..., I
n
:
theta
n
) = U
invoke
I(V
1
, V
2
, ..., V
n
)
Sample syntax:
D ::= ...|
define
I(FL)=U
FL ::= I:
theta
| I:
theta
, FL
U ::= ...|
invoke
I(AL)
AL ::= A | A, AL
A bit cumbersome for writing type rules.
Correspondence principle:
Binding of multiple parameters.
Multiple definition bindings (compound declaration)!
Alternative syntax:
D ::= ...|
define
I(F)=U
F ::= I:
theta
| F
1
, F
2
V ::= ...|
invoke
I(D)
Author:
Wolfgang Schreiner
Last Modification: May 7, 1998