stan/WLP2024
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add Unfold'

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-11-18 23:45:53 +01:00
parent 8413a6df05
commit a5b9cf1524
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
aspUnify.tex
View File

@ -313,6 +313,12 @@ described in chapter \ref{sec:translation}.
\type{T}_i \doteq \type{T}_i \type{T}_i \doteq \type{T}_i
} }
\and \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]{ \inferrule[Subst-Param]{
\type{T}' \doteq \type{S} \\ \type{T}' \doteq \type{S} \\
\type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\ \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\