Intensional Typing
•
Typing judgment
D
;
G
|- M : A
D
declares
expression variables
u :: A
G
declares
value variables
x : A
M is a
term
A is a
type
