[github pages] BRiCk documentation created from 43759fa8

docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.base_logic.lib.spectra.html

@@ -623,7 +623,7 @@ <h1 class="libtitle">bedrock.lang.base_logic.lib.spectra</h1>
 </div>
 
 <div class="doc">
-Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
+Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
     assumption in the hypothesis. 
 </div>
 <div class="code">
@@ -642,7 +642,7 @@ <h1 class="libtitle">bedrock.lang.base_logic.lib.spectra</h1>
 </div>
 
 <div class="doc">
-Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
+Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
     assumption in the hypothesis. 
 </div>
 <div class="code">
@@ -684,7 +684,7 @@ <h1 class="libtitle">bedrock.lang.base_logic.lib.spectra</h1>
 </div>
 
 <div class="doc">
-Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
+Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
     assumption in the hypothesis. 
 </div>
 <div class="code">
@@ -709,7 +709,7 @@ <h1 class="libtitle">bedrock.lang.base_logic.lib.spectra</h1>
 </div>
 
 <div class="doc">
-Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
+Stronger than the "obvious" statement thanks to the extra <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode">∈</span> <span class="inlinecode"><span class="id" title="var">STEP</span></span>
     assumption in the hypothesis. 
 </div>
 <div class="code">

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

@@ -347,7 +347,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.expr</h1>
 </div>
 
 <div class="doc">
-       <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#Emember_ignore"><span class="id" title="constructor">Emember_ignore</span></a></span> <span class="inlinecode"><span class="id" title="var">arrow</span></span> <span class="inlinecode"><span class="id" title="var">obj</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> represents:
+       <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#Emember_ignore"><span class="id" title="constructor">Emember_ignore</span></a></span> <span class="inlinecode"><span class="id" title="var">arrow</span></span> <span class="inlinecode"><span class="id" title="var">obj</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> represents:
 <ul class="doclist">
 <li> <code>obj-&gt;e</code> if <code>arrow = true</code>, or
 
@@ -1803,7 +1803,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.expr</h1>
 </div>
 
 <div class="doc">
-<span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#Ematerialize_temp"><span class="id" title="constructor">Ematerialize_temp</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> is an xvalue that gets memory (with automatic
+<span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#Ematerialize_temp"><span class="id" title="constructor">Ematerialize_temp</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> is an xvalue that gets memory (with automatic
         storage duration) and initializes it using the expression.
 
 </div>

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

@@ -732,8 +732,8 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.initializers</h1>
 
 <div class="paragraph"> </div>
 
-  <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.initializers.html#can_init"><span class="id" title="definition">can_init</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> is a side-condition for introducing <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.stmt.html#Stmt.wp_initialize"><span class="id" title="abbreviation">wp_initialize</span></a></span>
-  with value type <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> and expression <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span>, serving the conjunct <span class="inlinecode"><span class="id" title="var">v</span></span> <span class="inlinecode">=</span>
+  <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.initializers.html#can_init"><span class="id" title="definition">can_init</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> is a side-condition for introducing <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.stmt.html#Stmt.wp_initialize"><span class="id" title="abbreviation">wp_initialize</span></a></span>
+  with value type <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_init.ty"><span class="id" title="variable">ty</span></a></span> and expression <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span>, serving the conjunct <span class="inlinecode"><span class="id" title="var">v</span></span> <span class="inlinecode">=</span>
   <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.semantics.values.html#VAL_MIXIN.Vvoid"><span class="id" title="definition">Vvoid</span></a></span> in <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.initializers.html#wp_initialize_unqualified"><span class="id" title="module">wp_initialize_unqualified</span></a></span>'s <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#Tvoid"><span class="id" title="constructor">Tvoid</span></a></span> case.
 
 </div>

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

@@ -1330,7 +1330,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.wp</h1>
 
 <div class="paragraph"> </div>
 
- <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.wp_test"><span class="id" title="definition">wp_test</span></a></span> <span class="inlinecode">ρ</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.observe.html#example.Q"><span class="id" title="variable">Q</span></a></span> evaluates <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.with_cpp.wp_xval.e"><span class="id" title="variable">e</span></a></span> as an operand converting the value to a
+ <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.wp_test"><span class="id" title="definition">wp_test</span></a></span> <span class="inlinecode">ρ</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.observe.html#example.Q"><span class="id" title="variable">Q</span></a></span> evaluates <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.core.html#temp_arg.traverse.e"><span class="id" title="variable">e</span></a></span> as an operand converting the value to a
       boolean before passing it to <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.observe.html#example.Q"><span class="id" title="variable">Q</span></a></span>.
 
 </div>

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

@@ -131,7 +131,7 @@ <h1 class="libtitle">bedrock.lang.cpp.parser.expr</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Ecast"><span class="id" title="constructor">Ecast</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Cptr2int"><span class="id" title="constructor">Cptr2int</span></a> <a class="idref" href="bedrock.lang.cpp.parser.expr.html#t:15"><span class="id" title="variable">t</span></a>) <a class="idref" href="bedrock.lang.cpp.syntax.core.html#Enull"><span class="id" title="constructor">Enull</span></a>.<br/>
 
 <br/>
-&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="ParserExpr.Ealignof_preferred" class="idref" href="#ParserExpr.Ealignof_preferred"><span class="id" title="definition">Ealignof_preferred</span></a> (<a id="e:16" class="idref" href="#e:16"><span class="id" title="binder">e</span></a> : <a class="idref" href="bedrock.lang.cpp.parser.expr.html#ParserExpr.Expr"><span class="id" title="abbreviation">Expr</span></a>) (<a id="t:17" class="idref" href="#t:17"><span class="id" title="binder">t</span></a> : <a class="idref" href="bedrock.lang.cpp.parser.expr.html#ParserExpr.type"><span class="id" title="abbreviation">type</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="ParserExpr.Ealignof_preferred" class="idref" href="#ParserExpr.Ealignof_preferred"><span class="id" title="definition">Ealignof_preferred</span></a> (<a id="e:16" class="idref" href="#e:16"><span class="id" title="binder">e</span></a> : <a class="idref" href="bedrock.lang.cpp.parser.expr.html#ParserExpr.type"><span class="id" title="abbreviation">type</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</span></a> <a class="idref" href="bedrock.lang.cpp.parser.expr.html#ParserExpr.Expr"><span class="id" title="abbreviation">Expr</span></a>) (<a id="t:17" class="idref" href="#t:17"><span class="id" title="binder">t</span></a> : <a class="idref" href="bedrock.lang.cpp.parser.expr.html#ParserExpr.type"><span class="id" title="abbreviation">type</span></a>) :=<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Eunsupported"><span class="id" title="constructor">Eunsupported</span></a> "alignof_preferred" <a class="idref" href="bedrock.lang.cpp.parser.expr.html#t:17"><span class="id" title="variable">t</span></a>.<br/>
 
 <br/>