supercomb reduction doc

This commit is contained in:
crumbtoo
2023-11-14 12:17:29 -07:00
parent a10c5cb84b
commit 650e0a3cfe

View File

@@ -103,3 +103,24 @@ Restore the stack when a sub-computation has completed.
& g & g
} }
Reduce a supercombinator and update the root with the :math:`\beta`-reduced form
.. math::
\transrule
{ a_0 : a_1 : \ldots : a_n : s
& d
& h
\begin{bmatrix}
a_0 : \mathtt{NSupercomb} \; [x_1,\ldots,x_n] \; e
\end{bmatrix}
& g
}
{ a_n : s
& d
& h'
& g
\\
& \SetCell[c=3]{c}
\text{where } h' = \mathtt{instantiateU} \; e \; a_n \; h \; g
}