diff --git a/aspUnify.tex b/aspUnify.tex index fef62c8..cc059c2 100644 --- a/aspUnify.tex +++ b/aspUnify.tex @@ -313,6 +313,12 @@ described in chapter \ref{sec:translation}. \type{T}_i \doteq \type{T}_i } \and +\inferrule[Unfold']{ + \tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} +}{ + \type{T}_i \doteq \type{T}_i +} +\and \inferrule[Subst-Param]{ \type{T}' \doteq \type{S} \\ \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\