Go backward to Record Introduction Principle
Go up to Top
Go forward to Summary (Semantics)

Summary (Syntax)

Id: qualification.tex,v 1.2 1996/05/02 11:53:49 schreine Exp schreine

`pi` \|- D: `pi`₁`dec`	`pi` -U- `pi`₁ \|- U: `theta`
`pi` \|- begin D in U end: `theta`

`pi` \|- D₁: `pi`₁`dec`	`pi` -U- `pi`₁ \|- D₂: `pi`₂`dec`
`pi` \|- begin D in D₂ end: `pi`₂`dec`

`pi` \|- D: `pi`₁`dec`	`pi` -U- `pi`₁ \|- T: `deltaclass`
`pi` \|- begin D in T end: `deltaclass`

`pi` \|- D: `pi`₁`dec`	`pi` -U- `pi`₁ \|- C: `comm`
`pi` \|- begin D in C end: `comm`

`pi` \|- D: `pi`₁`dec`	`pi` -U- `pi`₁ \|- E: `tauexp`
`pi` \|- begin D in E end: `tauexp`