1 files changed, 24 insertions, 1 deletions
diff --git a/docs/doc/logic.html b/docs/doc/logic.html
index 6a69d995..9b18b817 100644
--- a/docs/doc/logic.html
+++ b/docs/doc/logic.html
@@ -72,8 +72,31 @@
     <span class='Function'>∨</span><span class='Modifier'>`</span> <span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span>
 ⟨ 0 1 1 1 1 1 1 ⟩
 </pre>
+<p>Not (<code><span class='Function'>¬</span></code>) isn't complicated: for example <code><span class='Function'>¬</span><span class='Value'>a</span><span class='Function'>=</span><span class='Value'>b</span></code> indicates that <code><span class='Value'>a</span></code> is <em>not</em> equal to <code><span class='Value'>b</span></code>. Or <code><span class='Value'>a</span><span class='Function'>≠</span><span class='Value'>b</span></code>, but you can't just put a slash through every symbol. One less obvious use is to convert a boolean to plus or minus 1, using the <a href="hook.html">hook</a> modifiers. <code><span class='Value'>b</span><span class='Function'>-¬</span><span class='Value'>b</span></code> leaves 1 unchanged but subtracts 1 from 0, while <code><span class='Paren'>(</span><span class='Function'>¬</span><span class='Value'>b</span><span class='Paren'>)</span><span class='Function'>-</span><span class='Value'>b</span></code> is the negation, converting 0 to 1 and 1 to ¯1.</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=LeKfnMKsIDDigL8xCgrCrOKKuC0gMOKAvzE=">↗️</a><pre>    <span class='Function'>-</span><span class='Modifier2'>⟜</span><span class='Function'>¬</span> <span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span>
+⟨ ¯1 1 ⟩
+
+    <span class='Function'>¬</span><span class='Modifier2'>⊸</span><span class='Function'>-</span> <span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span>
+⟨ 1 ¯1 ⟩
+</pre>
+<h3 id="span"><a class="header" href="#span">Span</a></h3>
+<p>Span isn't a logic function, given that <code><span class='Number'>1</span><span class='Function'>¬</span><span class='Number'>0</span></code> is <code><span class='Number'>2</span></code>, not a boolean. It's defined to be <code><span class='Number'>1</span><span class='Function'>+</span><span class='Value'>𝕨</span><span class='Function'>-</span><span class='Value'>𝕩</span></code> (I like to think of the line hanging off the right side as the 1 to be added). The reason it's called Span is that if the arguments are whole numbers with <code><span class='Value'>𝕩</span><span class='Function'>≤</span><span class='Value'>𝕨</span></code>, this is the length of the sequence <code><span class='Value'>𝕩</span><span class='Separator'>,</span> <span class='Value'>𝕩</span><span class='Function'>+</span><span class='Number'>1</span><span class='Separator'>,</span><span class='Value'>…</span> <span class='Value'>𝕨</span></code>.</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=NCDCrCAxICAgIyAxLCAyLCAzLCA0Cgo5IMKsIDcgICAjIDcsIDgsIDk=">↗️</a><pre>    <span class='Number'>4</span> <span class='Function'>¬</span> <span class='Number'>1</span>   <span class='Comment'># 1, 2, 3, 4
+</span>4
+
+    <span class='Number'>9</span> <span class='Function'>¬</span> <span class='Number'>7</span>   <span class='Comment'># 7, 8, 9
+</span>3
+</pre>
+<p>The fact that Not and Span share a glyph is no coincidence. <code><span class='Function'>¬</span><span class='Value'>𝕩</span></code> is <code><span class='Number'>0</span><span class='Function'>¬</span><span class='Value'>𝕩</span></code>, because this is equal to <code><span class='Number'>1</span><span class='Function'>-</span><span class='Value'>𝕩</span></code> and <code><span class='Number'>1</span><span class='Function'>-</span><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span></code> is <code><span class='Number'>1</span><span class='Ligature'>‿</span><span class='Number'>0</span></code>. And because <code><span class='Function'>¬</span><span class='Value'>𝕩</span></code> is defined to be <code><span class='Number'>1</span><span class='Function'>-</span><span class='Value'>𝕩</span></code> not just for booleans but for all numbers, it's also true that <code><span class='Value'>𝕨</span><span class='Function'>¬</span><span class='Value'>𝕩</span></code> is <code><span class='Value'>𝕨</span><span class='Function'>+¬</span><span class='Value'>𝕩</span></code>.</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=NSArIMKsIDDigL8x4oC/MQoKNSDCrCAw4oC/MeKAvzE=">↗️</a><pre>    <span class='Number'>5</span> <span class='Function'>+</span> <span class='Function'>¬</span> <span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span><span class='Ligature'>‿</span><span class='Number'>1</span>
+⟨ 6 5 5 ⟩
+
+    <span class='Number'>5</span> <span class='Function'>¬</span> <span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>1</span><span class='Ligature'>‿</span><span class='Number'>1</span>
+⟨ 6 5 5 ⟩
+</pre>
+<p>The identities <code><span class='Function'>¬</span><span class='Value'>𝕩</span> <span class='Gets'>←→</span> <span class='Number'>0</span><span class='Function'>¬</span><span class='Value'>𝕩</span></code> and <code><span class='Value'>𝕨</span><span class='Function'>¬</span><span class='Value'>𝕩</span> <span class='Gets'>←→</span> <span class='Value'>𝕨</span><span class='Function'>+¬</span><span class='Value'>𝕩</span></code> are also true with <code><span class='Function'>-</span></code> in place of <code><span class='Function'>¬</span></code>! That's because <code><span class='Function'>¬</span></code> is <code><span class='Brace'>{</span><span class='Number'>1</span><span class='Function'>+</span><span class='Value'>𝕨</span><span class='Function'>-</span><span class='Value'>𝕩</span><span class='Brace'>}</span></code>, or <code><span class='Number'>1</span><span class='Function'>+-</span></code>, in either case. Changing between <code><span class='Function'>-</span></code> and <code><span class='Function'>¬</span></code> only adds or subtracts 1 from both sides of the identities.</p>
 <h2 id="definitions"><a class="header" href="#definitions">Definitions</a></h2>
-<p>We define</p>
+<p>The three logic functions can be defined easily in terms of other arithmetic. They're convenience functions in that sense.</p>
 <pre><span class='Function'>Not</span> <span class='Gets'>←</span> <span class='Number'>1</span><span class='Function'>+-</span>  <span class='Comment'># also Span
 </span><span class='Function'>And</span> <span class='Gets'>←</span> <span class='Function'>×</span>
 <span class='Function'>Or</span>  <span class='Gets'>←</span> <span class='Function'>×</span><span class='Modifier2'>⌾</span><span class='Function'>¬</span>