Snapshot, will continue later

author: Ohad Kammar <ohad.kammar@ed.ac.uk> 2022-08-08 17:29:03 +0100
committer: Ohad Kammar <ohad.kammar@ed.ac.uk> 2022-08-08 17:29:03 +0100
commit: 63e894b39a82e5a8b1edd06f1e03e6bfc5aa8c81 (patch)
tree: 8eef9a4268a0b703318e8eb6d7e843caa72c2dc4
parent: 4032974f05f80cbab61a26f4b30ce57ec2e43b3b (diff)
4 files changed, 161 insertions, 25 deletions
diff --git a/doc/Tutorial.html b/doc/Tutorial.html
index e10bee7..23a7183 100644
--- a/doc/Tutorial.html
+++ b/doc/Tutorial.html
@@ -66,14 +66,14 @@
 <p><code class="IdrisCode"> <span class="IdrisKeyword">record</span> <span class="IdrisType">Equivalence</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">A</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Type</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">0</span> <span class="IdrisFunction">relation</span><span class="IdrisKeyword">:</span> <span class="IdrisFunction">Rel</span> <span class="IdrisBound">A</span><br />   <span class="IdrisFunction">reflexive</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span>       <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">x</span><br />   <span class="IdrisFunction">symmetric</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span>    <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">x</span><br />   <span class="IdrisFunction">transitive</span><span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">z</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">z</span><br />                             <span class="IdrisKeyword">-&gt;</span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">z</span><br /> </code></p>
 <p>We equip the built-in relation <code>Equal</code> with the structure of an equivalence relation, using the constructor <code>Refl</code> and the stdlib functions <code>sym</code>, and <code>trans</code>: <code class="IdrisCode"> <span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisBound">a</span><br /> <span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">(===)</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Refl</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisFunction">sym</span> <span class="IdrisBound">x_eq_y</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y_eq_z</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisFunction">trans</span> <span class="IdrisBound">x_eq_y</span> <span class="IdrisBound">y_eq_z</span><br />   <span class="IdrisKeyword">}</span><br /> </code></p>
 <p>We’ll use the following relation on pairs of natural numbers as a running example. We can represent an integer as the difference between a pair of natural numbers: <code class="IdrisCode"> <span class="IdrisKeyword">infix</span> <span class="IdrisKeyword">8</span> .-.<br /> <br /> <span class="IdrisKeyword">record</span> <span class="IdrisType">INT</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">(.-.)</span><br />   <span class="IdrisFunction">pos</span><span class="IdrisKeyword">,</span> <span class="IdrisFunction">neg</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br /> <br /> <span class="IdrisKeyword">record</span> <span class="IdrisType">SameDiff</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">INT</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />   constructor <span class="IdrisData">Check</span><br />   <span class="IdrisFunction">same</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">y</span><span class="IdrisFunction">.neg === </span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span><br /> </code> The <code>SameDiff x y</code> relation is equivalent to mathematical equation that states that the difference between the positive and negative parts is identical: <br /><span class="math display"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub> = <em>y</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>y</em><sub><em>n</em><em>e</em><em>g</em></sub></span><br /> But, unlike the last equation which requires us to define integers and subtraction, its equivalent <code>(.same)</code> is expressed using only addition, and so addition on <code>Nat</code> is enough.</p>
-<p>The relation <code>SameDiff</code> is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from <code>Syntax.PreorderReasoning</code>: <code class="IdrisCode"> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisType">INT</span><br /> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisType">SameDiff</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisData">Refl</span><span class="IdrisKeyword">)</span><br /> </code> This equational proof represents the single-step equational proof:</p>
-<p>&quot;Calculate:</p>
+<p>The relation <code>SameDiff</code> is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from <code>Syntax.PreorderReasoning</code>: <code class="IdrisCode"> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisType">INT</span><br /> <span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />   <span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisType">SameDiff</span><br />   <span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class="IdrisFunction"&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisData">Refl</span><span class="IdrisKeyword">)</span><br /> </code> This equational proof represents the single-step equational proof:</p>
+<p>"Calculate:</p>
 <ol type="1">
 <li><span class="math inline"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span></li>
-<li><span class="math inline"> = <em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span> (by reflexivity)&quot;</li>
+<li><span class="math inline"> = <em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span> (by reflexivity)"</li>
 </ol>
 <p>The mnemonic behind the ASCII-art is that the first step in the proof starts with a logical-judgement symbol <span class="math inline">⊢</span>, each step continues with an equality sign <span class="math inline">=</span>, and justified by a thought bubble <code>(...)</code>.</p>
-<p><code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">..&lt;</span><span class="IdrisKeyword">(</span><span class="IdrisBound">x_eq_y</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br /> </code> In this proof, we were given the proof <code>x_eq_y.same : x.pos + y.neg = y.pos + x.neg</code> and so we appealed to the symmetric equation. The mnemonic here is that the last bubble in the thought bubble <code>(...)</code> is replace with a left-pointing arrow, reversing the reasoning step. <code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y_eq_z</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;plusRightCancel&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;$</span> <span class="IdrisFunction">Calc</span> <span class="math inline">$&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;|~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;...&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;{&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Nat.Additive&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                   <span class="IdrisFunction">=-=</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">))</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span><span class="IdrisKeyword">)</span> <span class="math inline">$&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y\_eq\_z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.same&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;x&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;y&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.neg&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisBound&quot;&gt;z&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;...&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;(&lt;/span&gt;&lt;span class=&quot;IdrisFunction&quot;&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisData&quot;&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;{&lt;/span&gt;&lt;span class=&quot;IdrisBound&quot;&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisKeyword&quot;&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class=&quot;IdrisFunction&quot;&gt;Nat.Additive&lt;/span&gt;&lt;span class=&quot;IdrisKeyword&quot;&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">1</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span><span class="IdrisKeyword">)</span> ?h2<span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>   <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />                                      <span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">}</span><br /> </code> This proof is a lot more involved:</p>
+<p><code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class="IdrisFunction"&gt;Calc&lt;/span&gt;&amp;nbsp;$</span><br />       <span class="IdrisData">|~</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">..&lt;</span><span class="IdrisKeyword">(</span><span class="IdrisBound">x_eq_y</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br /> </code> In this proof, we were given the proof <code>x_eq_y.same : x.pos + y.neg = y.pos + x.neg</code> and so we appealed to the symmetric equation. The mnemonic here is that the last bubble in the thought bubble <code>(...)</code> is replace with a left-pointing arrow, reversing the reasoning step. <code class="IdrisCode">   <span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">&lt;/span&gt;<span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x_eq_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y_eq_z</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisData">Check</span> <span class="math inline">$&amp;nbsp;&lt;span class="IdrisFunction"&gt;plusRightCancel&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;\_&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;y&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;$</span> <span class="IdrisFunction">Calc</span> <span class="math inline">$&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class="IdrisData"&gt;|~&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;x&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;z&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.neg&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;y&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class="IdrisData"&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;x&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;(&lt;/span&gt;&lt;span class="IdrisBound"&gt;y&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;z&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.neg&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisData"&gt;...&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;(&lt;/span&gt;&lt;span class="IdrisFunction"&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisData"&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;{&lt;/span&gt;&lt;span class="IdrisBound"&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;Nat.Additive&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                   <span class="IdrisFunction">=-=</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">))</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span><span class="IdrisKeyword">)</span> <span class="math inline">$&amp;nbsp;&lt;span class="IdrisBound"&gt;y\_eq\_z&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.same&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;)&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class="IdrisData"&gt;~~&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;(&lt;/span&gt;&lt;span class="IdrisBound"&gt;x&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;y&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.neg&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;)&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;+&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisBound"&gt;z&lt;/span&gt;&lt;span class="IdrisFunction"&gt;.pos&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisData"&gt;...&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;(&lt;/span&gt;&lt;span class="IdrisFunction"&gt;solve&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisData"&gt;3&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;Monoid.Commutative.Free.Free&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;{&lt;/span&gt;&lt;span class="IdrisBound"&gt;a&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;=&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisFunction"&gt;Nat.Additive&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;}&lt;/span&gt;&amp;nbsp;$</span><br />                                      <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">1</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span><span class="IdrisKeyword">)</span> ?h2<span class="IdrisKeyword">)</span><br />       <span class="IdrisData">~~</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>   <span class="IdrisData">…</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />                                      <span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />                                      <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />                                  <span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span><span class="IdrisKeyword">)</span><br />   <span class="IdrisKeyword">}</span><br /> </code> This proof is a lot more involved:</p>
 <ol type="1">
 <li>We appeal to the cancellation property of addition: <span class="math inline"><em>a</em> + <em>c</em> = <em>b</em> + <em>c</em> ⇒ <em>a</em> = <em>b</em></span></li>
 </ol>
@@ -83,8 +83,9 @@
 </ol>
 <p>Here we use the idris library <a href="http://www.github.com/frex-project/idris-frex"><code>Frex</code></a> that can perform such routine rearrangements for common algebraic structures. In this case, we use the commutative monoid simplifier from <code>Frex</code>. If you want to read more about <code>Frex</code>, check the <a href="https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf">paper</a> out.</p>
 <p>Idris’s <code>Control.Relation</code> defines interfaces for properties like reflexivity and transitivity. While the setoid package doesn’t use them, we’ll use them in a few examples.</p>
-<p>The <code>Overlap</code> relation from Examples 1 and 2 is symmetric: <code class="IdrisCode"> Symm<span class="IdrisKeyword">e</span>tric (List a) Overlap where<br />   symmetric xs_overlaps_ys = Overlapping<br />     { common = xs_overlaps_ys.common<br />     , lhsPos = xs_overlaps_ys.rhsPos<br />     , rhsPos = xs_overlaps_ys.lhsPos<br />     }<br /> </code> However, <code>Overlap</code> is neither reflexive nor transitive:</p>
+<p>The <code>Overlap</code> relation from Examples 1 and 2 is symmetric: <code class="IdrisCode"> <span class="IdrisType">Symmetric</span> <span class="IdrisKeyword">(</span><span class="IdrisType">List</span> <span class="IdrisBound">a</span><span class="IdrisKeyword">)</span> <span class="IdrisType">Overlap</span> <span class="IdrisKeyword">where</span><br />   <span class="IdrisFunction">symmetric</span> <span class="IdrisBound">xs_overlaps_ys</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />     <span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs_overlaps_ys</span><span class="IdrisFunction">.common</span><br />     <span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs_overlaps_ys</span><span class="IdrisFunction">.rhsPos</span><br />     <span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs_overlaps_ys</span><span class="IdrisFunction">.lhsPos</span><br />     <span class="IdrisKeyword">}</span><br /> </code> However, <code>Overlap</code> is neither reflexive nor transitive:</p>
 <ul>
-<li><p>The empty list doesn’t overlap with itself: <code class="IdrisCode"> Ex3 : Not (Overlap [] [])<br /> Ex3 nil_overlaps_nil = case nil_overlaps_nil.lhsPos of<br /> <span class="IdrisFunction">  _</span> <span class="IdrisKeyword">i</span>m<span class="IdrisKeyword">p</span>o<span class="IdrisType">ssible</span><br /> </code></p></li>
-<li><p>Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> Ex<span class="IdrisData">4</span> <span class="IdrisData">: ( Overlap</span> <span class="IdrisData">[</span>1<span class="IdrisKeyword">]</span><span class="IdrisData"> [1,2</span>]<br />   <span class="IdrisData"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisBound">, Overlap [1,2] </span>[<span class="IdrisKeyword">2]</span><br />      <span class="IdrisData"> , No</span>t<span class="IdrisKeyword"> </span>(<span class="IdrisKeyword">Overlap [1</span>] [2]))<br /> Ex<span class="IdrisKeyword">4</span> =<br />   ( Overlapping 1 Here Here<br />   , Overlapping 2 (There Here) Here<br />   , &amp;nbsp;one_overlaps_two =&gt; case one_overlaps_two.lhsPos of<br />      There _ impossible<br />   )<br /> </code> The outer lists agree on <code>1</code> and <code>2</code>, respectively, but they can’t overlap on on the first element of either, which exhausts all possibilities of overlap.</p></li>
+<li><p>The empty list doesn’t overlap with itself: <code class="IdrisCode"> <span class="IdrisFunction">Ex3</span> <span class="IdrisKeyword">:</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[]</span> <span class="IdrisData">[]</span><span class="IdrisKeyword">)</span><br /> <span class="IdrisFunction">Ex3</span> <span class="IdrisBound">nil_overlaps_nil</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">nil_overlaps_nil</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br />   <span class="IdrisKeyword">_</span> <span class="IdrisKeyword">impossible</span><br /> </code></p></li>
+<li><p>Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> <span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[1,2]</span><br />       <span class="IdrisType">,</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2]</span> <span class="IdrisData">[2]</span><br />       <span class="IdrisType">,</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[2]</span><span class="IdrisKeyword">))</span><br /> <span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">=</span><br />   <span class="IdrisKeyword">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisData">Here</span> <span class="IdrisData">Here</span><br />   <span class="IdrisData">,</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">2</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span> <span class="IdrisData">Here</span><br />   <span class="IdrisData">,</span> <span class="IdrisKeyword">&lt;/span&gt; <span class="IdrisBound">one_overlaps_two</span> <span class="IdrisKeyword">=&gt;</span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">one_overlaps_two</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br />      <span class="IdrisData">There</span> <span class="IdrisKeyword">_</span> <span class="IdrisKeyword">impossible</span><br />   <span class="IdrisKeyword">)</span><br /> </code> The outer lists agree on <code>1</code> and <code>2</code>, respectively, but they can’t overlap on on the first element of either, which exhausts all possibilities of overlap.</p></li>
 </ul>
+<p><code class="IdrisCode"> <span class="IdrisBound">-</span>-<span class="IdrisFunction"> TO</span>D<span class="IdrisBound">O</span>:<span class="IdrisKeyword"> </span>c<span class="IdrisKeyword">l</span><span class="IdrisBound">e</span><span class="IdrisFunction">an t</span>h<span class="IdrisFunction">i</span>s<span class="IdrisBound"> </span><span class="IdrisFunction">up</span><br /> (.+.) : (x, y : INT) -&gt; INT<br /> <span class="IdrisFunction">x .+.</span> <span class="IdrisKeyword">y</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span><span class="IdrisKeyword">(</span>x<span class="IdrisBound">.</span>p<span class="IdrisKeyword">o</span>s<span class="IdrisType"> + </span><span class="IdrisKeyword">y</span>.<span class="IdrisKeyword">po</span>s<span class="IdrisType">) .</span>-. (x.neg + y.neg)<br /> <br /> (.*.) : (x, y : INT) -&gt; INT<br /> <span class="IdrisFunction">x</span><span class="IdrisKeyword"> </span>.<span class="IdrisFunction">*</span>.<span class="IdrisKeyword"> </span>y<span class="IdrisType"> = </span>(x.pos * y.pos + x.neg * y.neg) .-. (x.pos * y.neg + x.neg * y.pos)<br /> <br /> <span class="IdrisFunction">O</span>,<span class="IdrisKeyword"> </span>I<span class="IdrisData"> </span>:<span class="IdrisData"> IN</span>T<br /> <span class="IdrisFunction">O = 0 .-. 0</span><br /> <span class="IdrisFunction">I = 1 .-. 0</span><br /> plusIntZeroLftNeutral : (x : INT) -&gt; O .+. x <code>SameDiff</code> x<br /> <span class="IdrisFunction">plusIntZeroLftNeutral</span> <span class="IdrisKeyword">x</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span>C<span class="IdrisKeyword">h</span>e<span class="IdrisType">ck </span><span class="IdrisKeyword">R</span>e<span class="IdrisKeyword">fl</span><br /> <br /> plusIntZeroRgtNeutral : (x : INT) -&gt; <span class="IdrisKeyword">x</span><span class="IdrisBound"> </span>.<span class="IdrisKeyword">+</span>.<span class="IdrisFunction"> O <code>SameDiff&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;</code></span> x<br /> plusIntZeroRgtNeutral x = Check (solv<span class="IdrisKeyword">e</span><span class="IdrisFunction"> </span>2<span class="IdrisData"> </span>M<span class="IdrisFunction">ono</span>i<span class="IdrisFunction">d.</span><span class="IdrisKeyword">C</span>o<span class="IdrisFunction">mmu</span>t<span class="IdrisFunction">a</span>t<span class="IdrisData">i</span>ve.Free.Free<br />                                  <span class="IdrisFunction">   </span> <span class="IdrisFunction">{</span>a<span class="IdrisData"> </span>=<span class="IdrisFunction"> Na</span>t<span class="IdrisKeyword">.</span><span class="IdrisFunction">A</span>d<span class="IdrisData">d</span>i<span class="IdrisFunction">tiv</span>e<span class="IdrisFunction">} </span><span class="IdrisKeyword"><span class="math inline">$&lt;/span&gt;&lt;br /&gt; &amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;(X&amp;nbsp;0&amp;nbsp;.+.&amp;nbsp;O1)&amp;nbsp;.+.&amp;nbsp;X&amp;nbsp;1&lt;br /&gt; &lt;span class="IdrisFunction"&gt;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisBound"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisBound"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisBound"&gt;&amp;nbsp;&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisType"&gt;&amp;nbsp;&amp;nbsp;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;=&lt;/span&gt;-&lt;span class="IdrisKeyword"&gt;=&amp;nbsp;&lt;/span&gt;X&lt;span class="IdrisBound"&gt;&amp;nbsp;&lt;/span&gt;0&lt;span class="IdrisFunction"&gt;&amp;nbsp;.+&lt;/span&gt;.&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisBound"&gt;(&lt;/span&gt;X&lt;span class="IdrisFunction"&gt;&amp;nbsp;1&amp;nbsp;&lt;/span&gt;.&lt;span class="IdrisBound"&gt;+&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;.&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisType"&gt;O1))&lt;/span&gt;&lt;br /&gt; &lt;br /&gt; plusInrAssociative&amp;nbsp;:&amp;nbsp;(x,y,z&amp;nbsp;:&amp;nbsp;INT)&amp;nbsp;-&amp;gt;&lt;span class="IdrisKeyword"&gt;&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisBound"&gt;x&lt;/span&gt;&amp;nbsp;&lt;span class="IdrisKeyword"&gt;.&lt;/span&gt;+&lt;span class="IdrisFunction"&gt;.&amp;nbsp;(y&amp;nbsp;.+.&amp;nbsp;z)&amp;nbsp;&lt;/span&gt;&lt;span class="IdrisKeyword"&gt;`&lt;/span&gt;SameDiff`&amp;nbsp;(x&amp;nbsp;.+.&amp;nbsp;y)&amp;nbsp;.+.&amp;nbsp;z&lt;br /&gt; plusInrAssociative&amp;nbsp;x&amp;nbsp;y&amp;nbsp;z&amp;nbsp;=&amp;nbsp;Check&amp;nbsp;$</span><span class="IdrisKeyword"> </span><span class="IdrisFunction">(</span>s<span class="IdrisData">o</span>l<span class="IdrisFunction">ve </span>6<span class="IdrisKeyword"> </span><span class="IdrisFunction">M</span>o<span class="IdrisData">n</span>o<span class="IdrisFunction">id.</span>C<span class="IdrisFunction">o</span>m<span class="IdrisData">m</span><span class="IdrisKeyword">ut</span>a<span class="IdrisFunction">tiv</span>e<span class="IdrisKeyword">.F</span><span class="IdrisFunction">r</span>e<span class="IdrisData">e</span>.<span class="IdrisFunction">Fre</span>e<br />                                   <span class="IdrisFunction">   </span>{<span class="IdrisKeyword">a</span><span class="IdrisFunction"> </span>=<span class="IdrisData"> </span>N<span class="IdrisFunction">at.</span>A<span class="IdrisFunction">d</span>d<span class="IdrisData">i</span>t<span class="IdrisFunction">ive</span>}<span class="IdrisFunction"> </span>$<br />                                   (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)<br /> <span class="IdrisKeyword">    </span> <span class="IdrisType">    </span> <span class="IdrisKeyword"> </span> <span class="IdrisType">    </span> <span class="IdrisKeyword">     </span>            =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))<br /> <br /> da<span class="IdrisData">ta IN</span>T<span class="IdrisKeyword">‘</span> <span class="IdrisType">: T</span>y<span class="IdrisKeyword">pe</span> <span class="IdrisType">wher</span>e<br />   IPos  : Nat -&gt; INT’<br /> <span class="IdrisType">  IN</span>e<span class="IdrisType">gS :</span> <span class="IdrisType">Nat -&gt; </span>I<span class="IdrisKeyword">NT'</span><br /> <br /> Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">‘ Int</span>e<span class="IdrisBound">g</span><span class="IdrisKeyword">e</span>r<span class="IdrisKeyword"> </span>w<span class="IdrisFunction">h</span>e<span class="IdrisFunction">re</span><br />   cast (IPos k) = cast k<br /> <span class="IdrisType">  ca</span>s<span class="IdrisType">t (I</span>N<span class="IdrisType">egS</span> <span class="IdrisKeyword">k) = </span>- cast (S k)<br /> <br /> Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">' INT</span> <span class="IdrisBound">w</span><span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span>e<br />   cast (IPos k) = k .-. 0<br /> <span class="IdrisFunction">  cast (I</span>N<span class="IdrisKeyword">e</span>g<span class="IdrisType">S k</span>)<span class="IdrisKeyword"> =</span> <span class="IdrisType">0 .</span>-. (S k)<br /> <br /> <span class="IdrisFunction">normalise</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> IN</span><span class="IdrisData">T</span> <span class="IdrisBound">-</span><span class="IdrisKeyword">&gt;</span> <span class="IdrisData">INT</span><br /> <span class="IdrisFunction">normalise</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">i</span><br /> normalise i@((S k) .-. 0    ) = i<br /> <span class="IdrisFunction">normalise i@((S k) </span>.<span class="IdrisKeyword">-</span>.<span class="IdrisKeyword"> </span><span class="IdrisBound">(</span>S<span class="IdrisKeyword"> </span>j<span class="IdrisType">)) </span><span class="IdrisKeyword">=</span> <span class="IdrisKeyword">no</span>r<span class="IdrisType">malise</span> <span class="IdrisKeyword">(k</span><span class="IdrisFunction"> .-. j)</span><br /> <br /> <span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> (x</span><span class="IdrisData"> </span>:<span class="IdrisBound"> </span><span class="IdrisKeyword">I</span>N<span class="IdrisData">T) </span>-<span class="IdrisData">&gt;</span> Eit<span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span> <span class="IdrisData">((nor</span>m<span class="IdrisData">alis</span>e x).pos = Z) ((normalise x).neg = Z)<br /> <span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Left Refl</span><br /> normaliseEitherZero i@((S k) .-. 0    ) = Right Refl<br /> <span class="IdrisType">norm</span>a<span class="IdrisType">lis</span>e<span class="IdrisType">Eith</span>e<span class="IdrisKeyword">rZero</span> i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)<br /> <br /> Cast<span class="IdrisKeyword"> INT</span> <span class="IdrisFunction">INT' where</span><br />   cast<span class="IdrisKeyword"> </span><span class="IdrisData">x = </span>l<span class="IdrisBound">e</span><span class="IdrisKeyword">t</span> <span class="IdrisKeyword">(p</span>o<span class="IdrisKeyword">s .-</span>.<span class="IdrisBound"> ne</span>g<span class="IdrisKeyword">) </span>= normalise x in<br />     case<span class="IdrisData"> </span>n<span class="IdrisKeyword">or</span>m<span class="IdrisData">alis</span>e<span class="IdrisData">E</span>itherZero x of<br />       (L<span class="IdrisKeyword">e</span><span class="IdrisData">f</span>t<span class="IdrisBound"> </span><span class="IdrisKeyword">y</span>)<span class="IdrisKeyword"> =</span>&gt;<span class="IdrisData"> case</span> <span class="IdrisBound">n</span>eg of<br />       <span class="IdrisKeyword"> </span><span class="IdrisData"> 0 =&gt;</span> <span class="IdrisBound">I</span><span class="IdrisKeyword">P</span>o<span class="IdrisKeyword">s </span>0<br />         (S k) =&gt; INegS k<br /> <span class="IdrisComment">      (Right y) =&gt; IPo</span>s pos<br /> <br /> <span class="IdrisComment">– stuff you can show:</span><br /> <br /> <span class="IdrisBound">-</span>-<span class="IdrisFunction"> x </span><code>&lt;span class="IdrisBound"&gt;S&lt;/span&gt;a&lt;span class="IdrisKeyword"&gt;m&lt;/span&gt;e&lt;span class="IdrisFunction"&gt;Diff&lt;/span&gt;</code><span class="IdrisKeyword"> </span><span class="IdrisFunction">y -&gt;</span> <span class="IdrisBound">n</span>o<span class="IdrisFunction">rma</span>l<span class="IdrisFunction">ise </span>x<span class="IdrisBound"> </span><span class="IdrisKeyword">=</span> normalise y<br /> <span class="IdrisBound">(</span>:<span class="IdrisFunction">*:)</span>,<span class="IdrisBound"> </span>(<span class="IdrisKeyword">:</span>+<span class="IdrisFunction">:) :</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">x,y </span>:<span class="IdrisBound"> </span>I<span class="IdrisFunction">NT'</span>)<span class="IdrisFunction"> -&gt; </span>I<span class="IdrisBound">N</span><span class="IdrisKeyword">T</span>’<br /> x :+: y = cast (cast x .+. cast y)<br /> x :*: y = cast (cast x .*. cast y)<br /> <br /> </code></p>
diff --git a/doc/Tutorial.md b/doc/Tutorial.md
index b9a5896..439d245 100644
--- a/doc/Tutorial.md
+++ b/doc/Tutorial.md
@@ -241,34 +241,101 @@ setoid package doesn't use them, we'll use them in a few examples.
 
 The `Overlap` relation from Examples 1 and 2 is symmetric:
 <code class="IdrisCode">
-Symm<span class="IdrisKeyword">e</span>tric&nbsp;(List&nbsp;a)&nbsp;Overlap&nbsp;where<br />
-&nbsp;&nbsp;symmetric&nbsp;xs\_overlaps\_ys&nbsp;=&nbsp;Overlapping<br />
-&nbsp;&nbsp;&nbsp;&nbsp;{&nbsp;common&nbsp;=&nbsp;xs\_overlaps\_ys.common<br />
-&nbsp;&nbsp;&nbsp;&nbsp;,&nbsp;lhsPos&nbsp;=&nbsp;xs\_overlaps\_ys.rhsPos<br />
-&nbsp;&nbsp;&nbsp;&nbsp;,&nbsp;rhsPos&nbsp;=&nbsp;xs\_overlaps\_ys.lhsPos<br />
-&nbsp;&nbsp;&nbsp;&nbsp;}<br />
+<span class="IdrisType">Symmetric</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisType">List</span>&nbsp;<span class="IdrisBound">a</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisKeyword">where</span><br />
+&nbsp;&nbsp;<span class="IdrisFunction">symmetric</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisData">Overlapping</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span>&nbsp;<span class="IdrisBound">common</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.common</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">lhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.rhsPos</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">,</span>&nbsp;<span class="IdrisBound">rhsPos</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.lhsPos</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">}</span><br />
 </code>
 However, `Overlap` is neither reflexive nor transitive:
 
 * The empty list doesn't overlap with itself:
 <code class="IdrisCode">
-Ex3&nbsp;:&nbsp;Not&nbsp;(Overlap&nbsp;[]&nbsp;[])<br />
-Ex3&nbsp;nil\_overlaps\_nil&nbsp;=&nbsp;case&nbsp;nil\_overlaps\_nil.lhsPos&nbsp;of<br />
-<span class="IdrisFunction">&nbsp;&nbsp;\_</span>&nbsp;<span class="IdrisKeyword">i</span>m<span class="IdrisKeyword">p</span>o<span class="IdrisType">ssible</span><br />
+<span class="IdrisFunction">Ex3</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisFunction">Not</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[]</span>&nbsp;<span class="IdrisData">[]</span><span class="IdrisKeyword">)</span><br />
+<span class="IdrisFunction">Ex3</span>&nbsp;<span class="IdrisBound">nil\_overlaps\_nil</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">case</span>&nbsp;<span class="IdrisBound">nil\_overlaps\_nil</span><span class="IdrisFunction">.lhsPos</span>&nbsp;<span class="IdrisKeyword">of</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisKeyword">impossible</span><br />
 </code>
 
 * Two lists may overlap with a middle list, but on different elements. For example:
 <code class="IdrisCode">
-Ex<span class="IdrisData">4</span>&nbsp;<span class="IdrisData">:&nbsp;(&nbsp;Overlap</span>&nbsp;<span class="IdrisData">[</span>1<span class="IdrisKeyword">]</span><span class="IdrisData">&nbsp;[1,2</span>]<br />
-&nbsp;&nbsp;<span class="IdrisData">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisBound">,&nbsp;Overlap&nbsp;[1,2]&nbsp;</span>[<span class="IdrisKeyword">2]</span><br />
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">&nbsp;,&nbsp;No</span>t<span class="IdrisKeyword">&nbsp;</span>(<span class="IdrisKeyword">Overlap&nbsp;[1</span>]&nbsp;[2]))<br />
-Ex<span class="IdrisKeyword">4</span>&nbsp;=<br />
-&nbsp;&nbsp;(&nbsp;Overlapping&nbsp;1&nbsp;Here&nbsp;Here<br />
-&nbsp;&nbsp;,&nbsp;Overlapping&nbsp;2&nbsp;(There&nbsp;Here)&nbsp;Here<br />
-&nbsp;&nbsp;,&nbsp;\&nbsp;one\_overlaps\_two&nbsp;=&gt;&nbsp;case&nbsp;one\_overlaps\_two.lhsPos&nbsp;of<br />
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;There&nbsp;\_&nbsp;impossible<br />
-&nbsp;&nbsp;)<br />
+<span class="IdrisFunction">Ex4</span>&nbsp;<span class="IdrisKeyword">:</span>&nbsp;<span class="IdrisKeyword">(</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1]</span>&nbsp;<span class="IdrisData">[1,2]</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisType">,</span>&nbsp;<span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1,2]</span>&nbsp;<span class="IdrisData">[2]</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisType">,</span>&nbsp;<span class="IdrisFunction">Not</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span>&nbsp;<span class="IdrisData">[1]</span>&nbsp;<span class="IdrisData">[2]</span><span class="IdrisKeyword">))</span><br />
+<span class="IdrisFunction">Ex4</span>&nbsp;<span class="IdrisKeyword">=</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">(</span>&nbsp;<span class="IdrisData">Overlapping</span>&nbsp;<span class="IdrisData">1</span>&nbsp;<span class="IdrisData">Here</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisData">,</span>&nbsp;<span class="IdrisData">Overlapping</span>&nbsp;<span class="IdrisData">2</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisData">There</span>&nbsp;<span class="IdrisData">Here</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisData">Here</span><br />
+&nbsp;&nbsp;<span class="IdrisData">,</span>&nbsp;<span class="IdrisKeyword">\</span>&nbsp;<span class="IdrisBound">one\_overlaps\_two</span>&nbsp;<span class="IdrisKeyword">=&gt;</span>&nbsp;<span class="IdrisKeyword">case</span>&nbsp;<span class="IdrisBound">one\_overlaps\_two</span><span class="IdrisFunction">.lhsPos</span>&nbsp;<span class="IdrisKeyword">of</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">There</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisKeyword">impossible</span><br />
+&nbsp;&nbsp;<span class="IdrisKeyword">)</span><br />
 </code>
 The outer lists agree on `1` and `2`, respectively, but they can't overlap on
 on the first element of either, which exhausts all possibilities of overlap.
 
+
+
+<code class="IdrisCode">
+<span class="IdrisBound">-</span>-<span class="IdrisFunction">&nbsp;TO</span>D<span class="IdrisBound">O</span>:<span class="IdrisKeyword">&nbsp;</span>c<span class="IdrisKeyword">l</span><span class="IdrisBound">e</span><span class="IdrisFunction">an&nbsp;t</span>h<span class="IdrisFunction">i</span>s<span class="IdrisBound">&nbsp;</span><span class="IdrisFunction">up</span><br />
+(.+.)&nbsp;:&nbsp;(x,&nbsp;y&nbsp;:&nbsp;INT)&nbsp;-&gt;&nbsp;INT<br />
+<span class="IdrisFunction">x&nbsp;.+.</span>&nbsp;<span class="IdrisKeyword">y</span>&nbsp;<span class="IdrisKeyword">=</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">(</span>x<span class="IdrisBound">.</span>p<span class="IdrisKeyword">o</span>s<span class="IdrisType">&nbsp;+&nbsp;</span><span class="IdrisKeyword">y</span>.<span class="IdrisKeyword">po</span>s<span class="IdrisType">)&nbsp;.</span>-.&nbsp;(x.neg&nbsp;+&nbsp;y.neg)<br />
+<br />
+(.\*.)&nbsp;:&nbsp;(x,&nbsp;y&nbsp;:&nbsp;INT)&nbsp;-&gt;&nbsp;INT<br />
+<span class="IdrisFunction">x</span><span class="IdrisKeyword">&nbsp;</span>.<span class="IdrisFunction">\*</span>.<span class="IdrisKeyword">&nbsp;</span>y<span class="IdrisType">&nbsp;=&nbsp;</span>(x.pos&nbsp;\*&nbsp;y.pos&nbsp;+&nbsp;x.neg&nbsp;\*&nbsp;y.neg)&nbsp;.-.&nbsp;(x.pos&nbsp;\*&nbsp;y.neg&nbsp;+&nbsp;x.neg&nbsp;\*&nbsp;y.pos)<br />
+<br />
+<span class="IdrisFunction">O</span>,<span class="IdrisKeyword">&nbsp;</span>I<span class="IdrisData">&nbsp;</span>:<span class="IdrisData">&nbsp;IN</span>T<br />
+<span class="IdrisFunction">O&nbsp;=&nbsp;0&nbsp;.-.&nbsp;0</span><br />
+<span class="IdrisFunction">I&nbsp;=&nbsp;1&nbsp;.-.&nbsp;0</span><br />
+plusIntZeroLftNeutral&nbsp;:&nbsp;(x&nbsp;:&nbsp;INT)&nbsp;-&gt;&nbsp;O&nbsp;.+.&nbsp;x&nbsp;`SameDiff`&nbsp;x<br />
+<span class="IdrisFunction">plusIntZeroLftNeutral</span>&nbsp;<span class="IdrisKeyword">x</span>&nbsp;<span class="IdrisKeyword">=</span><span class="IdrisBound">&nbsp;</span>C<span class="IdrisKeyword">h</span>e<span class="IdrisType">ck&nbsp;</span><span class="IdrisKeyword">R</span>e<span class="IdrisKeyword">fl</span><br />
+<br />
+plusIntZeroRgtNeutral&nbsp;:&nbsp;(x&nbsp;:&nbsp;INT)&nbsp;-&gt;&nbsp;<span class="IdrisKeyword">x</span><span class="IdrisBound">&nbsp;</span>.<span class="IdrisKeyword">+</span>.<span class="IdrisFunction">&nbsp;O&nbsp;`SameDiff</span><span class="IdrisKeyword">`</span>&nbsp;x<br />
+plusIntZeroRgtNeutral&nbsp;x&nbsp;=&nbsp;Check&nbsp;(solv<span class="IdrisKeyword">e</span><span class="IdrisFunction">&nbsp;</span>2<span class="IdrisData">&nbsp;</span>M<span class="IdrisFunction">ono</span>i<span class="IdrisFunction">d.</span><span class="IdrisKeyword">C</span>o<span class="IdrisFunction">mmu</span>t<span class="IdrisFunction">a</span>t<span class="IdrisData">i</span>ve.Free.Free<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisFunction">{</span>a<span class="IdrisData">&nbsp;</span>=<span class="IdrisFunction">&nbsp;Na</span>t<span class="IdrisKeyword">.</span><span class="IdrisFunction">A</span>d<span class="IdrisData">d</span>i<span class="IdrisFunction">tiv</span>e<span class="IdrisFunction">}&nbsp;</span><span class="IdrisKeyword">$</span><br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(X&nbsp;0&nbsp;.+.&nbsp;O1)&nbsp;.+.&nbsp;X&nbsp;1<br />
+<span class="IdrisFunction">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisType">&nbsp;&nbsp;&nbsp;</span><span class="IdrisKeyword">=</span>-<span class="IdrisKeyword">=&nbsp;</span>X<span class="IdrisBound">&nbsp;</span>0<span class="IdrisFunction">&nbsp;.+</span>.<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">(</span>X<span class="IdrisFunction">&nbsp;1&nbsp;</span>.<span class="IdrisBound">+</span><span class="IdrisKeyword">.</span>&nbsp;<span class="IdrisType">O1))</span><br />
+<br />
+plusInrAssociative&nbsp;:&nbsp;(x,y,z&nbsp;:&nbsp;INT)&nbsp;-&gt;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">x</span>&nbsp;<span class="IdrisKeyword">.</span>+<span class="IdrisFunction">.&nbsp;(y&nbsp;.+.&nbsp;z)&nbsp;</span><span class="IdrisKeyword">`</span>SameDiff`&nbsp;(x&nbsp;.+.&nbsp;y)&nbsp;.+.&nbsp;z<br />
+plusInrAssociative&nbsp;x&nbsp;y&nbsp;z&nbsp;=&nbsp;Check&nbsp;$<span class="IdrisKeyword">&nbsp;</span><span class="IdrisFunction">(</span>s<span class="IdrisData">o</span>l<span class="IdrisFunction">ve&nbsp;</span>6<span class="IdrisKeyword">&nbsp;</span><span class="IdrisFunction">M</span>o<span class="IdrisData">n</span>o<span class="IdrisFunction">id.</span>C<span class="IdrisFunction">o</span>m<span class="IdrisData">m</span><span class="IdrisKeyword">ut</span>a<span class="IdrisFunction">tiv</span>e<span class="IdrisKeyword">.F</span><span class="IdrisFunction">r</span>e<span class="IdrisData">e</span>.<span class="IdrisFunction">Fre</span>e<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisFunction">&nbsp;&nbsp;&nbsp;</span>{<span class="IdrisKeyword">a</span><span class="IdrisFunction">&nbsp;</span>=<span class="IdrisData">&nbsp;</span>N<span class="IdrisFunction">at.</span>A<span class="IdrisFunction">d</span>d<span class="IdrisData">i</span>t<span class="IdrisFunction">ive</span>}<span class="IdrisFunction">&nbsp;</span>$<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(X&nbsp;0&nbsp;.+.&nbsp;(X&nbsp;1&nbsp;.+.&nbsp;X&nbsp;2))&nbsp;.+.&nbsp;((X&nbsp;3&nbsp;.+.&nbsp;X&nbsp;4)&nbsp;.+.&nbsp;X&nbsp;5)<br />
+<span class="IdrisKeyword">&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisType">&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisType">&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=-=&nbsp;(X&nbsp;0&nbsp;.+.&nbsp;X&nbsp;1&nbsp;.+.&nbsp;X&nbsp;2)&nbsp;.+.&nbsp;(X&nbsp;3&nbsp;.+.&nbsp;(X&nbsp;4&nbsp;.+.&nbsp;X&nbsp;5)))<br />
+<br />
+da<span class="IdrisData">ta&nbsp;IN</span>T<span class="IdrisKeyword">&apos;</span>&nbsp;<span class="IdrisType">:&nbsp;T</span>y<span class="IdrisKeyword">pe</span>&nbsp;<span class="IdrisType">wher</span>e<br />
+&nbsp;&nbsp;IPos&nbsp;&nbsp;:&nbsp;Nat&nbsp;-&gt;&nbsp;INT&apos;<br />
+<span class="IdrisType">&nbsp;&nbsp;IN</span>e<span class="IdrisType">gS&nbsp;:</span>&nbsp;<span class="IdrisType">Nat&nbsp;-&gt;&nbsp;</span>I<span class="IdrisKeyword">NT&apos;</span><br />
+<br />
+Ca<span class="IdrisFunction">st&nbsp;I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">&apos;&nbsp;Int</span>e<span class="IdrisBound">g</span><span class="IdrisKeyword">e</span>r<span class="IdrisKeyword">&nbsp;</span>w<span class="IdrisFunction">h</span>e<span class="IdrisFunction">re</span><br />
+&nbsp;&nbsp;cast&nbsp;(IPos&nbsp;k)&nbsp;=&nbsp;cast&nbsp;k<br />
+<span class="IdrisType">&nbsp;&nbsp;ca</span>s<span class="IdrisType">t&nbsp;(I</span>N<span class="IdrisType">egS</span>&nbsp;<span class="IdrisKeyword">k)&nbsp;=&nbsp;</span>-&nbsp;cast&nbsp;(S&nbsp;k)<br />
+<br />
+Ca<span class="IdrisFunction">st&nbsp;I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">&apos;&nbsp;INT</span>&nbsp;<span class="IdrisBound">w</span><span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span>e<br />
+&nbsp;&nbsp;cast&nbsp;(IPos&nbsp;k)&nbsp;=&nbsp;k&nbsp;.-.&nbsp;0<br />
+<span class="IdrisFunction">&nbsp;&nbsp;cast&nbsp;(I</span>N<span class="IdrisKeyword">e</span>g<span class="IdrisType">S&nbsp;k</span>)<span class="IdrisKeyword">&nbsp;=</span>&nbsp;<span class="IdrisType">0&nbsp;.</span>-.&nbsp;(S&nbsp;k)<br />
+<br />
+<span class="IdrisFunction">normalise</span>&nbsp;<span class="IdrisBound">:</span><span class="IdrisKeyword">&nbsp;IN</span><span class="IdrisData">T</span>&nbsp;<span class="IdrisBound">-</span><span class="IdrisKeyword">&gt;</span>&nbsp;<span class="IdrisData">INT</span><br />
+<span class="IdrisFunction">normalise</span>&nbsp;<span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData">&nbsp;</span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span>&nbsp;<span class="IdrisData">neg</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisData">&nbsp;</span>&nbsp;<span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;)</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">i</span><br />
+normalise&nbsp;i@((S&nbsp;k)&nbsp;.-.&nbsp;0&nbsp;&nbsp;&nbsp;&nbsp;)&nbsp;=&nbsp;i<br />
+<span class="IdrisFunction">normalise&nbsp;i@((S&nbsp;k)&nbsp;</span>.<span class="IdrisKeyword">-</span>.<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">(</span>S<span class="IdrisKeyword">&nbsp;</span>j<span class="IdrisType">))&nbsp;</span><span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisKeyword">no</span>r<span class="IdrisType">malise</span>&nbsp;<span class="IdrisKeyword">(k</span><span class="IdrisFunction">&nbsp;.-.&nbsp;j)</span><br />
+<br />
+<span class="IdrisFunction">normaliseEitherZero</span>&nbsp;<span class="IdrisBound">:</span><span class="IdrisKeyword">&nbsp;(x</span><span class="IdrisData">&nbsp;</span>:<span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">I</span>N<span class="IdrisData">T)&nbsp;</span>-<span class="IdrisData">&gt;</span>&nbsp;Eit<span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span>&nbsp;<span class="IdrisData">((nor</span>m<span class="IdrisData">alis</span>e&nbsp;x).pos&nbsp;=&nbsp;Z)&nbsp;((normalise&nbsp;x).neg&nbsp;=&nbsp;Z)<br />
+<span class="IdrisFunction">normaliseEitherZero</span>&nbsp;<span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData">&nbsp;</span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span>&nbsp;<span class="IdrisData">neg</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisData">&nbsp;</span>&nbsp;<span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;)</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Left&nbsp;Refl</span><br />
+normaliseEitherZero&nbsp;i@((S&nbsp;k)&nbsp;.-.&nbsp;0&nbsp;&nbsp;&nbsp;&nbsp;)&nbsp;=&nbsp;Right&nbsp;Refl<br />
+<span class="IdrisType">norm</span>a<span class="IdrisType">lis</span>e<span class="IdrisType">Eith</span>e<span class="IdrisKeyword">rZero</span>&nbsp;i@((S&nbsp;k)&nbsp;.-.&nbsp;(S&nbsp;j))&nbsp;=&nbsp;normaliseEitherZero&nbsp;(k&nbsp;.-.&nbsp;j)<br />
+<br />
+Cast<span class="IdrisKeyword">&nbsp;INT</span>&nbsp;<span class="IdrisFunction">INT&apos;&nbsp;where</span><br />
+&nbsp;&nbsp;cast<span class="IdrisKeyword">&nbsp;</span><span class="IdrisData">x&nbsp;=&nbsp;</span>l<span class="IdrisBound">e</span><span class="IdrisKeyword">t</span>&nbsp;<span class="IdrisKeyword">(p</span>o<span class="IdrisKeyword">s&nbsp;.-</span>.<span class="IdrisBound">&nbsp;ne</span>g<span class="IdrisKeyword">)&nbsp;</span>=&nbsp;normalise&nbsp;x&nbsp;in<br />
+&nbsp;&nbsp;&nbsp;&nbsp;case<span class="IdrisData">&nbsp;</span>n<span class="IdrisKeyword">or</span>m<span class="IdrisData">alis</span>e<span class="IdrisData">E</span>itherZero&nbsp;x&nbsp;of<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(L<span class="IdrisKeyword">e</span><span class="IdrisData">f</span>t<span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">y</span>)<span class="IdrisKeyword">&nbsp;=</span>&gt;<span class="IdrisData">&nbsp;case</span>&nbsp;<span class="IdrisBound">n</span>eg&nbsp;of<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisData">&nbsp;0&nbsp;=&gt;</span>&nbsp;<span class="IdrisBound">I</span><span class="IdrisKeyword">P</span>o<span class="IdrisKeyword">s&nbsp;</span>0<br />
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(S&nbsp;k)&nbsp;=&gt;&nbsp;INegS&nbsp;k<br />
+<span class="IdrisComment">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(Right&nbsp;y)&nbsp;=&gt;&nbsp;IPo</span>s&nbsp;pos<br />
+<br />
+<span class="IdrisComment">--&nbsp;stuff&nbsp;you&nbsp;can&nbsp;show:</span><br />
+<br />
+<span class="IdrisBound">-</span>-<span class="IdrisFunction">&nbsp;x&nbsp;</span>`<span class="IdrisBound">S</span>a<span class="IdrisKeyword">m</span>e<span class="IdrisFunction">Diff</span>`<span class="IdrisKeyword">&nbsp;</span><span class="IdrisFunction">y&nbsp;-&gt;</span>&nbsp;<span class="IdrisBound">n</span>o<span class="IdrisFunction">rma</span>l<span class="IdrisFunction">ise&nbsp;</span>x<span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">=</span>&nbsp;normalise&nbsp;y<br />
+<span class="IdrisBound">(</span>:<span class="IdrisFunction">\*:)</span>,<span class="IdrisBound">&nbsp;</span>(<span class="IdrisKeyword">:</span>+<span class="IdrisFunction">:)&nbsp;:</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisFunction">x,y&nbsp;</span>:<span class="IdrisBound">&nbsp;</span>I<span class="IdrisFunction">NT&apos;</span>)<span class="IdrisFunction">&nbsp;-&gt;&nbsp;</span>I<span class="IdrisBound">N</span><span class="IdrisKeyword">T</span>&apos;<br />
+x&nbsp;:+:&nbsp;y&nbsp;=&nbsp;cast&nbsp;(cast&nbsp;x&nbsp;.+.&nbsp;cast&nbsp;y)<br />
+x&nbsp;:\*:&nbsp;y&nbsp;=&nbsp;cast&nbsp;(cast&nbsp;x&nbsp;.\*.&nbsp;cast&nbsp;y)<br />
+<br />
+</code>
+
diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg
index b97fb59..9bce2e7 100644
--- a/doc/setoid-doc.ipkg
+++ b/doc/setoid-doc.ipkg
@@ -19,6 +19,7 @@ depends
   , frex
 modules
   = Tutorial
+  , Minh
 
 -- name of executable
 sourcedir = "sources"
diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md
index a33652f..68dda37 100644
--- a/doc/sources/Tutorial.md
+++ b/doc/sources/Tutorial.md
@@ -251,3 +251,70 @@ Ex4 =
 ```
 The outer lists agree on `1` and `2`, respectively, but they can't overlap on
 on the first element of either, which exhausts all possibilities of overlap.
+
+
+
+```idris
+-- TODO: clean this up
+(.+.) : (x, y : INT) -> INT
+x .+. y = (x.pos + y.pos) .-. (x.neg + y.neg)
+
+(.*.) : (x, y : INT) -> INT
+x .*. y = (x.pos * y.pos + x.neg * y.neg) .-. (x.pos * y.neg + x.neg * y.pos)
+
+O, I : INT
+O = 0 .-. 0
+I = 1 .-. 0
+plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x
+plusIntZeroLftNeutral x = Check Refl
+
+plusIntZeroRgtNeutral : (x : INT) -> x .+. O `SameDiff` x
+plusIntZeroRgtNeutral x = Check (solve 2 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                     (X 0 .+. O1) .+. X 1
+                                 =-= X 0 .+. (X 1 .+. O1))
+
+plusInrAssociative : (x,y,z : INT) -> x .+. (y .+. z) `SameDiff` (x .+. y) .+. z
+plusInrAssociative x y z = Check $ (solve 6 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                  (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)
+                                  =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))
+
+data INT' : Type where
+  IPos  : Nat -> INT'
+  INegS : Nat -> INT'
+
+Cast INT' Integer where
+  cast (IPos k) = cast k
+  cast (INegS k) = - cast (S k)
+
+Cast INT' INT where
+  cast (IPos k) = k .-. 0
+  cast (INegS k) = 0 .-. (S k)
+
+normalise : INT -> INT
+normalise i@(0 .-. neg      ) = i
+normalise i@((S k) .-. 0    ) = i
+normalise i@((S k) .-. (S j)) = normalise (k .-. j)
+
+normaliseEitherZero : (x : INT) -> Either ((normalise x).pos = Z) ((normalise x).neg = Z)
+normaliseEitherZero i@(0 .-. neg      ) = Left Refl
+normaliseEitherZero i@((S k) .-. 0    ) = Right Refl
+normaliseEitherZero i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)
+
+Cast INT INT' where
+  cast x = let (pos .-. neg) = normalise x in
+    case normaliseEitherZero x of
+      (Left y) => case neg of
+        0 => IPos 0
+        (S k) => INegS k
+      (Right y) => IPos pos
+
+-- stuff you can show:
+
+-- x `SameDiff` y -> normalise x = normalise y
+(:*:), (:+:) : (x,y : INT') -> INT'
+x :+: y = cast (cast x .+. cast y)
+x :*: y = cast (cast x .*. cast y)
+
+```
author	Ohad Kammar <ohad.kammar@ed.ac.uk>	2022-08-08 17:29:03 +0100
committer	Ohad Kammar <ohad.kammar@ed.ac.uk>	2022-08-08 17:29:03 +0100
commit	63e894b39a82e5a8b1edd06f1e03e6bfc5aa8c81 (patch)
tree	8eef9a4268a0b703318e8eb6d7e843caa72c2dc4
parent	4032974f05f80cbab61a26f4b30ce57ec2e43b3b (diff)