Specify function Undo headers

1 files changed, 2 insertions, 0 deletions

diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html
index 2ff3ce0a..bda3e054 100644
--- a/docs/spec/inferred.html
+++ b/docs/spec/inferred.html
@@ -470,6 +470,8 @@
 </tr>
 </tbody>
 </table>
+<h3 id="undo-headers">Undo headers</h3>
+<p>An <code><span class='Function'>UndoHead</span></code> header specifies how a block function acts when undone. Like ordinary headers, undo headers are searched for a match when a block function <code><span class='Function'>F</span></code> is undone, or when <code><span class='Function'>F</span><span class='Modifier'>˜</span></code> is undone with two arguments (including the two modifier cases <code><span class='Function'>𝔽</span><span class='Modifier2'>⟜</span><span class='Value'>k</span></code> and <code><span class='Function'>𝔽𝔾</span><span class='Value'>k</span></code> from the previous section). An <code><span class='Function'>UndoHead</span></code> without <code><span class='String'>&quot;˜&quot;</span></code> matches the <code><span class='Function'>F</span><span class='Modifier'>⁼</span></code> case while one with <code><span class='String'>&quot;˜&quot;</span></code> matches the <code><span class='Function'>F</span><span class='Modifier'>˜⁼</span></code> case. The left and right arguments are matched to <code><span class='Value'>headW</span></code> and <code><span class='Value'>headX</span></code> as with ordinary headers, and the first matching case is evaluated to give the result of the Undo-derived function.</p>
 <h2 id="under">Under</h2>
 <p>The Under 2-modifier <code><span class='Modifier2'>⌾</span></code> conceptually applies its left operand under the action of its right operand. Setting <code><span class='Value'>z</span><span class='Gets'>←</span><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier2'>⌾</span><span class='Function'>𝔾</span><span class='Value'>𝕩</span></code>, it satisfies <code><span class='Paren'>(</span><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier2'>○</span><span class='Function'>𝔾</span><span class='Value'>𝕩</span><span class='Paren'>)</span> <span class='Function'>≡</span> <span class='Function'>𝔾</span><span class='Value'>z</span></code>. We might say that <code><span class='Function'>𝔾</span></code> transforms values to a new domain, and <code><span class='Modifier2'>⌾</span><span class='Function'>𝔾</span></code> lifts actions <code><span class='Function'>𝔽</span></code> performed in this domain to the original domain of values. For example, addition in the logarithmic domain corresponds to multiplication in the linear domain: <code><span class='Function'>+</span><span class='Modifier2'>⌾</span><span class='Paren'>(</span><span class='Function'>⋆</span><span class='Modifier'>⁼</span><span class='Paren'>)</span></code> is <code><span class='Function'>×</span></code> (but less precise if computed in floating point).</p>
 <p>Let <code><span class='Value'>v</span><span class='Gets'>←</span><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier2'>○</span><span class='Function'>𝔾</span><span class='Value'>𝕩</span></code>, so that <code><span class='Value'>v</span><span class='Function'>≡𝔾</span><span class='Value'>z</span></code>. <code><span class='Value'>v</span></code> is of course well-defined, so the inference step is to find <code><span class='Value'>z</span></code> based on <code><span class='Value'>v</span></code> and possibly the original inputs. We distinguish three cases for Under:</p>