[github pages] BRiCk documentation created from 0ec27097

docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.stmt.html

@@ -526,7 +526,8 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.stmt</h1>
 <br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C++&nbsp;(and&nbsp;C)&nbsp;allow&nbsp;optimizing&nbsp;away&nbsp;certain&nbsp;infinite&nbsp;loops,<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;e.g.&nbsp;&lt;&lt;while&nbsp;(1);&gt;&gt;&nbsp;can&nbsp;be&nbsp;optimized&nbsp;to&nbsp;&lt;&lt;;&gt;&gt;.<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;These&nbsp;loop&nbsp;rules&nbsp;are&nbsp;not&nbsp;sound&nbsp;for&nbsp;use&nbsp;with&nbsp;compilations&nbsp;that&nbsp;use&nbsp;this&nbsp;optimization.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;These&nbsp;loop&nbsp;rules&nbsp;are&nbsp;not&nbsp;sound&nbsp;for&nbsp;use&nbsp;with&nbsp;compilations&nbsp;that&nbsp;use&nbsp;this<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;optimization.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
 
 <br/>
@@ -827,7 +828,8 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.stmt</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#s:350"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">with</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sseq"><span class="id" title="constructor">Sseq</span></a> <span class="id" title="var">ls</span> =&gt; <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#forallb"><span class="id" title="definition">forallb</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <span class="id" title="var">ls</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sdecl"><span class="id" title="constructor">Sdecl</span></a> <span class="id" title="var">_</span> =&gt; <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sif"><span class="id" title="constructor">Sif</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#::bool_scope:x_'&amp;&amp;'_x"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <span class="id" title="var">b</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sif"><span class="id" title="constructor">Sif</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sif_consteval"><span class="id" title="constructor">Sif_consteval</span></a> <span class="id" title="var">a</span> <span class="id" title="var">b</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#::bool_scope:x_'&amp;&amp;'_x"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <span class="id" title="var">b</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Swhile"><span class="id" title="constructor">Swhile</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">s</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#s:350"><span class="id" title="variable">s</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sfor"><span class="id" title="constructor">Sfor</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">s</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#s:350"><span class="id" title="variable">s</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sdo"><span class="id" title="constructor">Sdo</span></a> <span class="id" title="var">s</span> <span class="id" title="var">_</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#no_case:351"><span class="id" title="definition">no_case</span></a> <a class="idref" href="bedrock.lang.cpp.logic.stmt.html#s:350"><span class="id" title="variable">s</span></a><br/>

docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.parser.stmt.html

@@ -62,10 +62,6 @@ <h1 class="libtitle">bedrock.lang.cpp.parser.stmt</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;(<a id="init:6" class="idref" href="#init:6"><span class="id" title="binder">init</span></a> : <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Stmt"><span class="id" title="abbreviation">Stmt</span></a>) (<a id="cond:7" class="idref" href="#cond:7"><span class="id" title="binder">cond</span></a> : <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Expr"><span class="id" title="abbreviation">Expr</span></a>) (<a id="inc:8" class="idref" href="#inc:8"><span class="id" title="binder">inc</span></a> : <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Expr"><span class="id" title="abbreviation">Expr</span></a>)<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;(<a id="decl:9" class="idref" href="#decl:9"><span class="id" title="binder">decl</span></a> <a id="body:10" class="idref" href="#body:10"><span class="id" title="binder">body</span></a> : <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Stmt"><span class="id" title="abbreviation">Stmt</span></a>) : <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Stmt"><span class="id" title="abbreviation">Stmt</span></a> :=<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sseq"><span class="id" title="constructor">Sseq</span></a> (<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#option_list"><span class="id" title="definition">option_list</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#init:6"><span class="id" title="variable">init</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c6"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="bedrock.lang.cpp.parser.stmt.html#range:3"><span class="id" title="variable">range</span></a><a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#ibegin:4"><span class="id" title="variable">ibegin</span></a><a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#iend:5"><span class="id" title="variable">iend</span></a><a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sfor"><span class="id" title="constructor">Sfor</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#cond:7"><span class="id" title="variable">cond</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#inc:8"><span class="id" title="variable">inc</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sseq"><span class="id" title="constructor">Sseq</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a><a class="idref" href="bedrock.lang.cpp.parser.stmt.html#decl:9"><span class="id" title="variable">decl</span></a><a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#body:10"><span class="id" title="variable">body</span></a><a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>)<a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>).<br/>
-
-<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="Sif_consteval" class="idref" href="#Sif_consteval"><span class="id" title="definition">Sif_consteval</span></a> (<span class="id" title="var">_</span> <span class="id" title="var">_</span> : <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Expr"><span class="id" title="abbreviation">Expr</span></a>) : <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#Stmt"><span class="id" title="abbreviation">Stmt</span></a> :=<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Sunsupported"><span class="id" title="constructor">Sunsupported</span></a> "if consteval".<br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="bedrock.lang.cpp.parser.stmt.html#stmt"><span class="id" title="section">stmt</span></a>.<br/>
 </div>
 <!--