Go backward to
Typing Rules
Go up to
Top
Go forward to
Example
Record Introduction
Abstraction/qualification principle:
E ::= ...| I=E |E
1
,E
2
|
with
E
1
do
E
2
| I
pi
|- E:
theta
pi
|- I=E: {I:
theta
}
pi
|- E
1
:
pi
1
pi
|- E
2
:
pi
2
pi
|- E
1
,E
2
:
pi
1
U
pi
2
pi
|- E
1
:
pi
1
pi
-U-
pi
1
|- E
2
:
theta
pi
|-
with
E
1
do
E
2
:
theta
pi
|- I:
theta
if (I:
theta
) in
pi
Record
I=E
Record union E
1
,E
2
.
Local record definitions.
Record field reference
I
.
Enrichement of type system:
Type attribute for records.
{
i
:
theta
i
}
i
in
I
Type assignment attributes introduced.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: records.tex,v 1.1 1996/05/20 12:33:10 schreine Exp schreine