Merge pull request #49 from yforster/snipped

Change snippet on frontpage

src/rocqproverorg_frontend/pages/home_snippet.eml

@@ -1,20 +1,32 @@
 let render =
 <div class="alectryon-root alectryon-centered"><div class="document">
-<pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Definition</span> <span class="nf">square</span> <span class="nv">x</span> := x * x.</span><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk0"><span class="kn">Eval</span> <span class="nb">compute</span> <span class="kr">in</span> square <span class="mi">3</span>.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">= <span class="mi">9</span>
-: nat</blockquote></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Fixpoint</span> <span class="nf">fac</span> <span class="nv">n</span> :=
+<pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk0"><span class="kn">Require Import</span> Lia.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">[Loading ML file ring_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</blockquote><blockquote class="alectryon-message">[Loading ML file zify_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</blockquote><blockquote class="alectryon-message">[Loading ML file micromega_core_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</blockquote><blockquote class="alectryon-message">[Loading ML file micromega_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</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="kn">Fixpoint</span> <span class="nf">fac</span> <span class="nv">n</span> :=
   <span class="kr">match</span> n <span class="kr">with</span>
   | <span class="mi">0</span> | <span class="mi">1</span> =&gt; <span class="mi">1</span>
   | S n&#39; =&gt; n * fac n&#39;
   <span class="kr">end</span>.</span><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk1"><span class="kn">Eval</span> <span class="nb">compute</span> <span class="kr">in</span> fac <span class="mi">5</span>.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">= <span class="mi">120</span>
+</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk1"><span class="kn">Eval</span> <span class="nb">compute</span> <span class="kr">in</span> fac <span class="mi">5</span>.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">= <span class="mi">120</span>
 : nat</blockquote></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk2" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk2"><span class="kn">Lemma</span> <span class="nf">square_pos</span> : <span class="kr">forall</span> <span class="nv">n</span>, n &gt; <span class="mi">0</span> -&gt; square n &gt; <span class="mi">0</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="kr">forall</span> <span class="nv">n</span> : nat, n &gt; <span class="mi">0</span> -&gt; square n &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk3" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk3"><span class="kn">Proof</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="kr">forall</span> <span class="nv">n</span> : nat, n &gt; <span class="mi">0</span> -&gt; square n &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-wsp">   </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk4" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk4"><span class="nb">induction</span> n <span class="kr">as</span> [|n IHn].</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="mi">0</span> &gt; <span class="mi">0</span> -&gt; square <span class="mi">0</span> &gt; <span class="mi">0</span></div></blockquote><div class="alectryon-extra-goals"><input class="alectryon-extra-goal-toggle" id="square-v-chk5" style="display: none" type="checkbox"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>n &gt; <span class="mi">0</span> -&gt; square n &gt; <span class="mi">0</span></span></span></span><br></div><label class="goal-separator" for="square-v-chk5"><hr></label><div class="goal-conclusion">S n &gt; <span class="mi">0</span> -&gt; square (S n) &gt; <span class="mi">0</span></div></blockquote></div></div></div></small><span class="alectryon-wsp">
-</span></span><span class="alectryon-wsp">   </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk6" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk6">-</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="mi">0</span> &gt; <span class="mi">0</span> -&gt; square <span class="mi">0</span> &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="nb">trivial</span>.</span><span class="alectryon-wsp">
-</span></span><span class="alectryon-wsp">   </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="square-v-chk7" style="display: none" type="checkbox"><label class="alectryon-input" for="square-v-chk7">-</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>n &gt; <span class="mi">0</span> -&gt; square n &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">S n &gt; <span class="mi">0</span> -&gt; square (S n) &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="bp">now</span> <span class="nb">unfold</span> square; <span class="bp">lia</span>.</span><span class="alectryon-wsp">
-</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Qed</span>.</span></span>
-</pre>
-                                        </div>
+</span></span><span class="alectryon-wsp">
+</span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk2" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk2"><span class="kn">Lemma</span> <span class="nf">fac_pos</span> <span class="nv">n</span> : fac n &gt; <span class="mi">0</span>.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac n &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk3" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk3"><span class="kn">Proof</span>.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac n &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk4" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk4"><span class="nb">induction</span> n.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion">fac <span class="mi">0</span> &gt; <span class="mi">0</span></div></blockquote><div class="alectryon-extra-goals"><input class="alectryon-extra-goal-toggle" id="rocq-v-chk5" style="display: none" type="checkbox"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac n &gt; <span class="mi">0</span></span></span></span><br></div><label class="goal-separator" for="rocq-v-chk5"><hr></label><div class="goal-conclusion">fac (S n) &gt; <span class="mi">0</span></div></blockquote></div></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk6" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk6">-</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><span class="goal-separator"><hr></span><div class="goal-conclusion">fac <span class="mi">0</span> &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk7" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk7"><span class="nb">unfold</span> fac.</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="mi">1</span> &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="bp">lia</span>.</span><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">  </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk8" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk8">-</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac n &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac (S n) &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chk9" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chk9"><span class="nb">destruct</span> n.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac <span class="mi">0</span> &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac <span class="mi">1</span> &gt; <span class="mi">0</span></div></blockquote><div class="alectryon-extra-goals"><input class="alectryon-extra-goal-toggle" id="rocq-v-chka" style="display: none" type="checkbox"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac (S n) &gt; <span class="mi">0</span></span></span></span><br></div><label class="goal-separator" for="rocq-v-chka"><hr></label><div class="goal-conclusion">fac (S (S n)) &gt; <span class="mi">0</span></div></blockquote></div></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chkb" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chkb">+</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac <span class="mi">0</span> &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac <span class="mi">1</span> &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chkc" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chkc"><span class="nb">unfold</span> fac.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac <span class="mi">0</span> &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="mi">1</span> &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="bp">lia</span>.</span><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">    </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chkd" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chkd">+</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>n</var><span class="hyp-type"><b>: </b><span>nat</span></span></span><br><span><var>IHn</var><span class="hyp-type"><b>: </b><span>fac (S n) &gt; <span class="mi">0</span></span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">fac (S (S n)) &gt; <span class="mi">0</span></div></blockquote></div></div></small><span class="alectryon-wsp"> </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="nb">unfold</span> fac <span class="kr">in</span> *; <span class="bp">lia</span>.</span><span class="alectryon-wsp">
+</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Qed</span>.</span><span class="alectryon-wsp">
+</span></span><span class="alectryon-wsp">
+</span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chke" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chke"><span class="kn">Require Import</span> <span class="kn">Extraction</span>.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">[Loading ML file extraction_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</blockquote></div></div></small><span class="alectryon-wsp">
+</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Extraction Language OCaml</span>.</span><span class="alectryon-wsp">
+</span></span><span class="alectryon-sentence"><input class="alectryon-toggle" id="rocq-v-chkf" style="display: none" type="checkbox"><label class="alectryon-input" for="rocq-v-chkf"><span class="kn">Extraction</span> fac.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message"><span class="sd">(** val fac : nat -&gt; nat **)</span>
+
+<span class="kr">let rec</span> <span class="nv">fac</span> <span class="nv">n</span> = <span class="kr">match</span> n <span class="kr">with</span>
+| O -&gt; S O
+| S n&#39; -&gt;
+  (<span class="kr">match</span> n&#39; <span class="kr">with</span>
+   | O -&gt; S O
+   | S _ -&gt; mul n (fac n&#39;))</blockquote></div></div></small></span></pre>
+</div>