For sake of readability, we only describe simplified rules covering all
cases.
|
|
| |
| ⟨p : αp; q: τq; 1⟩
=
⟨p : τp; r : τr; 1⟩
= e |
|
| ⟨p : αp; q : τq;
r : τr; 1⟩ = e
∧ αp = τp |
|
|
| |
| ⟨p : τp; 1⟩ =
⟨p : αp; q : τq; 0⟩
= e |
|
| ⟨p : τp; q : τq; 0⟩
= e ∧ αp = τp |
|
| |
| ⟨p : τp; 0⟩ =
⟨p : αp; 0⟩ = e |
|
| ⟨p : αp; 0⟩ = e
∧ αp = τp |
|
|
| |
| ⟨q : τq; 0⟩ =
⟨r : τr; 0⟩ = e |
|
| ⊥ |
|
|
|
The generalization is obvious:
the occurrences of
p:αp, p:τp,
q:τq, and r:τr,
can be replaced by finite mappings from labels to types
P, P',
Q, and R of disjoint
domain except for P and P' of identical domain.These (generalized) rules should be added to those for simple types,
where rule Fail and Decompose are not extended
to the object type constructor, nor the row constructors.