From 650e0a3cfe5c4d42dda97dfe5828fb3b4e46d06d Mon Sep 17 00:00:00 2001
From: crumbtoo <crumb@disroot.org>
Date: Tue, 14 Nov 2023 12:17:29 -0700
Subject: [PATCH] supercomb reduction doc

---
 docs/src/commentary/stg.rst | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/docs/src/commentary/stg.rst b/docs/src/commentary/stg.rst
index e123621..8fdac9b 100644
--- a/docs/src/commentary/stg.rst
+++ b/docs/src/commentary/stg.rst
@@ -103,3 +103,24 @@ Restore the stack when a sub-computation has completed.
    & 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
+   }
+