Go backward to Typing RulesGo up to TopGo forward to Example |

- Abstraction/qualification principle:
- E ::= ...| I=E |E
,E_{1}|_{2}`with`E_{1}`do`E| I_{2} -
`pi`|- E:`theta``pi`|- I=E: {I:`theta`}

`pi`|- E:_{1}`pi`_{1}`pi`|- E:_{2}`pi`_{2}`pi`|- E,E_{1}:_{2}`pi`U_{1}`pi`_{2}

`pi`|- E:_{1}`pi`_{1}`pi`-U-`pi`|- E_{1}:_{2}`theta``pi`|-`with`E_{1}`do`E:_{2}`theta`

if (I:`pi`|- I:`theta``theta`) in`pi`

- E ::= ...| I=E |E
- Record I=E
- Record union E
,E_{1}._{2} - Local record definitions.
- Record field reference
*I*.

- Record union E
- Enrichement of type system:
- Type attribute for records.
- {
*i*:`theta`}_{i}_{i in I} - Type assignment attributes introduced.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998