recipes: Rebuild output

Author: cpitclaudel

recipes/output/coqdoc.html

@@ -1,3 +1,3 @@
-<pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="fragments-json-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="fragments-json-chk0"><span class="highlight"><span class="kn">Example</span> <span class="nf">xyz</span> (<span class="nv">H</span>: <span class="kt">False</span>): <span class="kt">True</span>. <span class="c">(* ... *)</span></span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>H</var><span><span class="hyp-type"><b>:</b><span class="highlight"><span class="kt">False</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kt">True</span></span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="bp">exact</span> I.</span></span><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><!-- alectryon-block-end -->
+<pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="fragments-json-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="fragments-json-chk0"><span class="highlight"><span class="kn">Example</span> <span class="nf">xyz</span> (<span class="nv">H</span>: <span class="kt">False</span>): <span class="kt">True</span>. <span class="c">(* ... *)</span></span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>H</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="kt">False</span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kt">True</span></span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="bp">exact</span> I.</span></span><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Qed</span>.</span></span></span></pre><!-- alectryon-block-end -->
 <pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="fragments-json-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="fragments-json-chk1"><span class="highlight"><span class="kn">Print</span> xyz.</span></label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message"><span class="highlight">xyz = <span class="kr">fun</span> <span class="nv">_</span> : <span class="kt">False</span> =&gt; I
      : <span class="kt">False</span> -&gt; <span class="kt">True</span></span></blockquote></div></div></small></span></pre><!-- alectryon-block-end -->

recipes/output/coqdoc.v.html

@@ -21,10 +21,10 @@
 <pre class="alectryon-io"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk0"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">Gauss</span>: <span class="kr">∀</span> <span class="nv">n</span>,
     <span class="mi">2</span> * (nsum n (<span class="kr">fun</span> <span class="nv">x</span> =&gt; x)) =
     n * (n + <span class="mi">1</span>).</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">∀</span> <span class="nv">n</span> : nat, <span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = n * (n + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk1"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">cbn</span> [nsum].</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * <span class="mi">0</span> = <span class="mi">0</span> * (<span class="mi">0</span> + <span class="mi">1</span>)</span></div></blockquote><div class="alectryon-extra-goals"><input class="alectryon-extra-goal-toggle" id="hyps-rst-chk2" style="display: none" type="checkbox"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>n</var><span><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></span></div><div><var>IHn</var><span><span class="hyp-type"><b>:</b><span class="highlight"><span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = n * (n + <span class="mi">1</span>)</span></span></span></div></div><label class="goal-separator" for="hyps-rst-chk2"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * (S n + nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x)) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk1"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">cbn</span> [nsum].</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * <span class="mi">0</span> = <span class="mi">0</span> * (<span class="mi">0</span> + <span class="mi">1</span>)</span></div></blockquote><div class="alectryon-extra-goals"><input class="alectryon-extra-goal-toggle" id="hyps-rst-chk2" style="display: none" type="checkbox"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div><div><var>IHn</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = n * (n + <span class="mi">1</span>)</span></span></div></div><label class="goal-separator" for="hyps-rst-chk2"><hr></label><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * (S n + nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x)) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></div></small><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk3" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk3"><span class="highlight">- <span class="c">(* n ← 0 *)</span></span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * <span class="mi">0</span> = <span class="mi">0</span> * (<span class="mi">0</span> + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="bp">reflexivity</span>.</span></span><span class="alectryon-wsp">
-</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk4" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk4"><span class="highlight">- <span class="c">(* n ← S _ *)</span></span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>n</var><span><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></span></div><div><var>IHn</var><span><span class="hyp-type"><b>:</b><span class="highlight"><span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = n * (n + <span class="mi">1</span>)</span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * (S n + nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x)) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk4" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk4"><span class="highlight">- <span class="c">(* n ← S _ *)</span></span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><div><var>n</var><span class="hyp-type"><b>:</b><span class="highlight">nat</span></span></div><div><var>IHn</var><span class="hyp-type"><b>:</b><span class="highlight"><span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = n * (n + <span class="mi">1</span>)</span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * (S n + nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x)) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk5" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk5"><span class="highlight"><span class="nb">rewrite</span> Mult.mult_plus_distr_l.</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * S n + <span class="mi">2</span> * nsum n (<span class="kr">λ</span> <span class="nv">x</span> : nat, x) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><input checked="checked" class="alectryon-toggle" id="hyps-rst-chk6" style="display: none" type="checkbox"><label class="alectryon-input" for="hyps-rst-chk6"><span class="highlight"><span class="nb">rewrite</span> IHn.</span></label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="mi">2</span> * S n + n * (n + <span class="mi">1</span>) = S n * (S n + <span class="mi">1</span>)</span></div></blockquote></div></div></small><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="bp">ring</span>.</span></span><span class="alectryon-wsp">