[github pages] BRiCk documentation created from 43759fa8

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

@@ -692,7 +692,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.expr</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.bi.prelude.html#0582ac70d883d93be3a66ac50f1c9225"><span class="id" title="notation">(</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#c221b9dad79b2807ca5890fdbaa6e59d"><span class="id" title="notation">letI</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#c221b9dad79b2807ca5890fdbaa6e59d"><span class="id" title="notation">*</span></a> <a class="idref" href="bedrock.lang.bi.prelude.html#c221b9dad79b2807ca5890fdbaa6e59d"><span class="id" title="notation">'</span></a><a id="pat:295" class="idref" href="#pat:295"><span class="id" title="binder">(</span></a><a id="la:294" class="idref" href="#la:294"><span class="id" title="binder"><span id="pat:295" class="id">la</span></span></a><a id="pat:295" class="idref" href="#pat:295"><span class="id" title="binder">,</span></a> <a id="rv:293" class="idref" href="#rv:293"><span class="id" title="binder"><span id="pat:295" class="id">rv</span></span></a><a id="pat:295" class="idref" href="#pat:295"><span class="id" title="binder">)</span></a>, <a id="free:296" class="idref" href="#free:296"><span class="id" title="binder">free</span></a> <a class="idref" href="bedrock.lang.bi.prelude.html#c221b9dad79b2807ca5890fdbaa6e59d"><span class="id" title="notation">:=</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.eval2"><span class="id" title="definition">eval2</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#evaluation_order.order_of"><span class="id" title="definition">evaluation_order.order_of</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#OOEqual"><span class="id" title="constructor">OOEqual</span></a>) (<a class="idref" href="bedrock.lang.cpp.logic.expr.html#Expr.wp_lval"><span class="id" title="abbreviation">wp_lval</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#l:290"><span class="id" title="variable">l</span></a>) (<a class="idref" href="bedrock.lang.cpp.logic.expr.html#Expr.wp_operand"><span class="id" title="abbreviation">wp_operand</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#r:291"><span class="id" title="variable">r</span></a>) <a class="idref" href="bedrock.lang.bi.prelude.html#c221b9dad79b2807ca5890fdbaa6e59d"><span class="id" title="notation">in</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.cpp.logic.expr.html#la:294"><span class="id" title="variable">la</span></a> <a class="idref" href="bedrock.lang.cpp.logic.rep_defs.html#62731479375849aa261b6fbaae1406e9"><span class="id" title="notation">|-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.heap_pred.html#anyR"><span class="id" title="abbreviation">anyR</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.types.html#erase_qualifiers"><span class="id" title="definition">erase_qualifiers</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#ty:289"><span class="id" title="variable">ty</span></a>) (<a class="idref" href="bedrock.lang.cpp.algebra.cfrac.html#cQp.mut"><span class="id" title="abbreviation">cQp.mut</span></a> 1) <a class="idref" href="bedrock.lang.bi.prelude.html#edd4b90f66987f0e4145840adec59ece"><span class="id" title="notation">**</span></a><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.bi.prelude.html#edd4b90f66987f0e4145840adec59ece"><span class="id" title="notation">(</span></a><a class="idref" href="bedrock.lang.cpp.logic.expr.html#la:294"><span class="id" title="variable">la</span></a> <a class="idref" href="bedrock.lang.cpp.logic.rep_defs.html#62731479375849aa261b6fbaae1406e9"><span class="id" title="notation">|-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.heap_pred.html#primR"><span class="id" title="abbreviation">primR</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.types.html#erase_qualifiers"><span class="id" title="definition">erase_qualifiers</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#ty:289"><span class="id" title="variable">ty</span></a>) (<a class="idref" href="bedrock.lang.cpp.algebra.cfrac.html#cQp.mut"><span class="id" title="abbreviation">cQp.mut</span></a> 1) <a class="idref" href="bedrock.lang.cpp.logic.expr.html#rv:293"><span class="id" title="variable">rv</span></a> <a class="idref" href="bedrock.lang.bi.prelude.html#1ceed28b6e47de516f82862d053216fa"><span class="id" title="notation">-*</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#Q:292"><span class="id" title="variable">Q</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#la:294"><span class="id" title="variable">la</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#free:296"><span class="id" title="variable">free</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#edd4b90f66987f0e4145840adec59ece"><span class="id" title="notation">)</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#0582ac70d883d93be3a66ac50f1c9225"><span class="id" title="notation">)</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.bi.prelude.html#edd4b90f66987f0e4145840adec59ece"><span class="id" title="notation">(</span></a><a class="idref" href="bedrock.lang.cpp.logic.expr.html#la:294"><span class="id" title="variable">la</span></a> <a class="idref" href="bedrock.lang.cpp.logic.rep_defs.html#62731479375849aa261b6fbaae1406e9"><span class="id" title="notation">|-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.heap_pred.html#tptstoR"><span class="id" title="abbreviation">tptstoR</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.types.html#erase_qualifiers"><span class="id" title="definition">erase_qualifiers</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#ty:289"><span class="id" title="variable">ty</span></a>) (<a class="idref" href="bedrock.lang.cpp.algebra.cfrac.html#cQp.mut"><span class="id" title="abbreviation">cQp.mut</span></a> 1) <a class="idref" href="bedrock.lang.cpp.logic.expr.html#rv:293"><span class="id" title="variable">rv</span></a> <a class="idref" href="bedrock.lang.bi.prelude.html#1ceed28b6e47de516f82862d053216fa"><span class="id" title="notation">-*</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#Q:292"><span class="id" title="variable">Q</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#la:294"><span class="id" title="variable">la</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#free:296"><span class="id" title="variable">free</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#edd4b90f66987f0e4145840adec59ece"><span class="id" title="notation">)</span></a><a class="idref" href="bedrock.lang.bi.prelude.html#0582ac70d883d93be3a66ac50f1c9225"><span class="id" title="notation">)</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="bedrock.lang.bi.prelude.html#0582ac70d883d93be3a66ac50f1c9225"><span class="id" title="notation">|--</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#Expr.wp_lval"><span class="id" title="abbreviation">wp_lval</span></a> (<a class="idref" href="bedrock.lang.cpp.syntax.core.html#Eassign"><span class="id" title="constructor">Eassign</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#l:290"><span class="id" title="variable">l</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#r:291"><span class="id" title="variable">r</span></a> <a class="idref" href="bedrock.lang.cpp.logic.expr.html#ty:289"><span class="id" title="variable">ty</span></a>) <a class="idref" href="bedrock.lang.cpp.logic.expr.html#Q:292"><span class="id" title="variable">Q</span></a>.<br/>
 
 <br/>