** Next:** Expression Typing
** Up:** Static Semantics
** Previous:** Record Disjointness
** Contents**

##

Definitional Equality

We use
to stand for a one-hole context that, when filled, yields a constructor. The notation
plugs
into
. We omit the standard definition of one-hole contexts. We write
for capture-avoiding substitution of
for
in
, with analogous notation for substituting a kind in a constructor.

2014-07-14