| Expression
Types |
|
|
|
|
|
|
|
|
|
| A
terms denoting expressions of type A |
||||||||
| Introduction
rule (constructor) |
||||||||
| D ; |- E : A |
||||||||
| D ; G |- box E : A |
||||||||
| E
depends only on expression variables! |
||||||||
