[github pages] BRiCk documentation created from e602a964

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

@@ -266,7 +266,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.cstring</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">by</span> <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Lists.List.html#map_id"><span class="id" title="lemma">map_id</span></a>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;** <span class="id" title="tactic">apply</span> <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring.WFs_equiv"><span class="id" title="lemma">WFs_equiv</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">Hhead</span> [<span class="id" title="var">Hty</span> [<span class="id" title="var">Hnonzero</span> <span class="id" title="var">Hnull</span>]]].<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.ZArith.BinInt.html#Z.of_nat"><span class="id" title="definition">Z.of_nat</span></a> (<a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n0</span>) <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring.strlen"><span class="id" title="abbreviation">strlen</span></a> (<span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">zs</span>)) <span class="id" title="keyword">as</span> <span class="id" title="var">Hn</span><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">by</span> (<span class="id" title="tactic">unfold</span> <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring._strlen"><span class="id" title="definition">strlen</span></a>, <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring._size"><span class="id" title="definition">size</span></a>; <span class="id" title="tactic">rewrite</span> <a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#cons_length"><span class="id" title="definition">cons_length</span></a> <span class="id" title="var">Hlen'</span>; <span class="id" title="var">lia</span>).<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">by</span> (<span class="id" title="tactic">unfold</span> <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring._strlen"><span class="id" title="definition">strlen</span></a>, <a class="idref" href="bedrock.lang.cpp.logic.zstring.html#zstring._size"><span class="id" title="definition">size</span></a>; <span class="id" title="tactic">rewrite</span> <a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#length_cons"><span class="id" title="definition">length_cons</span></a> <span class="id" title="var">Hlen'</span>; <span class="id" title="var">lia</span>).<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">specialize</span> (<span class="id" title="var">Hnull</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n0</span>) <span class="id" title="var">Hn</span>); <span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">Hnull</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> -<span class="id" title="var">Hnull</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">under</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Lists.List.html#map_ext_in"><span class="id" title="lemma">map_ext_in</span></a> =&gt; <span class="id" title="var">x</span> <span class="id" title="var">HIn</span>. 1: {<br/>

docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.heap_pred.everywhere.html

@@ -515,7 +515,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.heap_pred.everywhere</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iDestruct</span> "B" <span class="id" title="keyword">as</span> (<span class="id" title="var">f</span>) "B". <span class="id" title="var">iExists</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">f</span>).<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="var">iFrame</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <a class="idref" href="bedrock.lang.cpp.logic.arr.html#arrayR_eq"><span class="id" title="definition">arrayR_eq</span></a>/<a class="idref" href="bedrock.lang.cpp.logic.arr.html#arrayR_def"><span class="id" title="definition">arrayR_def</span></a> <a class="idref" href="bedrock.lang.cpp.logic.arr.html#arrR_eq"><span class="id" title="definition">arrR_eq</span></a>/<a class="idref" href="bedrock.lang.cpp.logic.arr.html#arrR_def"><span class="id" title="definition">arrR_def</span></a>.<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iFrame</span>. <span class="id" title="tactic">rewrite</span> !<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#fmap_length"><span class="id" title="lemma">fmap_length</span></a>. <span class="id" title="var">done</span>. }<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iFrame</span>. <span class="id" title="tactic">rewrite</span> !<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#length_fmap"><span class="id" title="lemma">length_fmap</span></a>. <span class="id" title="var">done</span>. }<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" title="var">case_match</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">iIntros</span> "[]".<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">case_match</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">iIntros</span> "[]".<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" title="tactic">rewrite</span> /<a class="idref" href="bedrock.lang.cpp.logic.heap_pred.everywhere.html#union_defR"><span class="id" title="definition">union_defR</span></a>.<br/>

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

@@ -368,7 +368,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.object_repr</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" title="var">iIntros</span> "P"; <span class="id" title="var">iDestruct</span> "P" <span class="id" title="keyword">as</span> (<span class="id" title="var">sz'</span>) "[%Hsz' #tptrs]".<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> !<a class="idref" href="bedrock.lang.cpp.logic.rep.html#_at_sep"><span class="id" title="lemma">_at_sep</span></a> !<a class="idref" href="bedrock.lang.cpp.logic.rep.html#_at_offsetR"><span class="id" title="lemma">_at_offsetR</span></a> !<a class="idref" href="bedrock.lang.cpp.logic.rep.html#_at_only_provable"><span class="id" title="lemma">_at_only_provable</span></a>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.option.html#is_Some"><span class="id" title="definition">is_Some</span></a> (<a class="idref" href="bedrock.lang.cpp.semantics.types.html#size_of"><span class="id" title="definition">size_of</span></a> <a class="idref" href="bedrock.lang.cpp.logic.object_repr.html#d11d71f9e358f88e8e3f36d78db1fb81"><span class="id" title="variable">σ</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.types.html#Tu8"><span class="id" title="abbreviation">Tu8</span></a>)) <span class="id" title="tactic">by</span> <span class="id" title="tactic">eauto</span>; <span class="id" title="var">iFrame</span> "%".<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#fmap_length"><span class="id" title="lemma">fmap_length</span></a> -<span class="id" title="lemma">to_nat_lengthN</span> <span class="id" title="var">Hlen</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.ZArith.Znat.html#N_nat_Z"><span class="id" title="lemma">N_nat_Z</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#length_fmap"><span class="id" title="lemma">length_fmap</span></a> -<span class="id" title="lemma">to_nat_lengthN</span> <span class="id" title="var">Hlen</span> <a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.ZArith.Znat.html#N_nat_Z"><span class="id" title="lemma">N_nat_Z</span></a>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">Hsz'</span> <span class="id" title="tactic">in</span> <span class="id" title="var">Hsz</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hsz</span>; <span class="id" title="tactic">subst</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">iSplit</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" title="tactic">rewrite</span> (<a class="idref" href="https://plv.mpi-sws.org/coqdoc/iris//iris.bi.big_op.html#big_sepL_lookup"><span class="id" title="lemma">big_sepL_lookup</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.19.0/stdlib//Coq.Arith.PeanoNat.html#Nat.pred"><span class="id" title="definition">Nat.pred</span></a> (<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.base.html#length"><span class="id" title="abbreviation">length</span></a> <span class="id" title="var">xs</span>))). 2: {<br/>

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

@@ -260,7 +260,7 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.raw</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> <span class="id" title="var">rs2</span>; [| <span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">Hlen</span>; <span class="id" title="var">lia</span>].<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> /<a class="idref" href="bedrock.lang.bi.observe.html#Observe2"><span class="id" title="class">Observe2</span></a>; <span class="id" title="var">iIntros</span> "? ? !&gt;"; <span class="id" title="tactic">by</span> <span class="id" title="var">iPureIntro</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> <span class="id" title="var">rs2</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">r2</span> ?]; [<span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">Hlen</span>; <span class="id" title="var">lia</span> |].<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> !<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#cons_length"><span class="id" title="definition">cons_length</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Hlen</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hlen</span>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> !<a class="idref" href="https://plv.mpi-sws.org/coqdoc/stdpp//stdpp.list.html#length_cons"><span class="id" title="definition">length_cons</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Hlen</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hlen</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> /<a class="idref" href="bedrock.lang.cpp.logic.raw.html#rawsR"><span class="id" title="definition">rawsR</span></a> !<a class="idref" href="bedrock.lang.cpp.logic.arr.html#arrayR_cons"><span class="id" title="lemma">arrayR_cons</span></a>;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">fold</span> (<a class="idref" href="bedrock.lang.cpp.logic.raw.html#rawsR"><span class="id" title="definition">rawsR</span></a> <span class="id" title="var">q1</span> <span class="id" title="var">rs1</span>);<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">fold</span> (<a class="idref" href="bedrock.lang.cpp.logic.raw.html#rawsR"><span class="id" title="definition">rawsR</span></a> <span class="id" title="var">q2</span> <span class="id" title="var">rs2</span>).<br/>