[github pages] BRiCk documentation created from 8d02ab5

docs/_static/coqdoc/bedrock.lang.algebra.big_op.html

@@ -56,11 +56,11 @@ <h1 class="libtitle">bedrock.lang.algebra.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab66"></a><h1 class="section">Big ops</h1>
+<a id="lab67"></a><h1 class="section">Big ops</h1>
 
 <div class="paragraph"> </div>
 
-<a id="lab67"></a><h2 class="section"><span class="inlinecode"><a class="idref" href="bedrock.lang.algebra.big_op.html#set_seq"><span class="id" title="section">set_seq</span></a></span></h2>
+<a id="lab68"></a><h2 class="section"><span class="inlinecode"><a class="idref" href="bedrock.lang.algebra.big_op.html#set_seq"><span class="id" title="section">set_seq</span></a></span></h2>
 
 </div>
 <div class="code">
@@ -77,7 +77,7 @@ <h1 class="libtitle">bedrock.lang.algebra.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab68"></a><h2 class="section">Powers and big ops</h2>
+<a id="lab69"></a><h2 class="section">Powers and big ops</h2>
 
 <div class="paragraph"> </div>
 
@@ -173,7 +173,7 @@ <h1 class="libtitle">bedrock.lang.algebra.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab69"></a><h2 class="section">Powers encoded as big ops</h2>
+<a id="lab70"></a><h2 class="section">Powers encoded as big ops</h2>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.algebra.coGset.html

@@ -80,7 +80,7 @@ <h1 class="libtitle">bedrock.lang.algebra.coGset</h1>
 Misplaced: Upstream to <span class="inlinecode"><span class="id" title="var">iris.algebra.coGset</span></span>? 
 <div class="paragraph"> </div>
 
-<a id="lab64"></a><h1 class="section">The union CMRA</h1>
+<a id="lab65"></a><h1 class="section">The union CMRA</h1>
 
 </div>
 <div class="code">
@@ -166,7 +166,7 @@ <h1 class="libtitle">bedrock.lang.algebra.coGset</h1>
 </div>
 
 <div class="doc">
-<a id="lab65"></a><h1 class="section">The disjoint union CMRA</h1>
+<a id="lab66"></a><h1 class="section">The disjoint union CMRA</h1>
 
 </div>
 <div class="code">

docs/_static/coqdoc/bedrock.lang.algebra.monoid.html

@@ -55,7 +55,7 @@ <h1 class="libtitle">bedrock.lang.algebra.monoid</h1>
 </div>
 
 <div class="doc">
-<a id="lab70"></a><h1 class="section">Powers in monoids</h1>
+<a id="lab71"></a><h1 class="section">Powers in monoids</h1>
  Overview:
 
 <div class="paragraph"> </div>

docs/_static/coqdoc/bedrock.lang.bi.atomic_commit.html

@@ -70,7 +70,7 @@ <h1 class="libtitle">bedrock.lang.bi.atomic_commit</h1>
 </div>
 
 <div class="doc">
-<a id="lab76"></a><h1 class="section">Atomic commits</h1>
+<a id="lab77"></a><h1 class="section">Atomic commits</h1>
  Atomic commits are atomic updates without abort. 
 </div>
 <div class="code">

docs/_static/coqdoc/bedrock.lang.bi.big_op.html

@@ -57,7 +57,7 @@ <h1 class="libtitle">bedrock.lang.bi.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab94"></a><h2 class="section">Lists</h2>
+<a id="lab95"></a><h2 class="section">Lists</h2>
 
 </div>
 <div class="code">
@@ -329,7 +329,7 @@ <h1 class="libtitle">bedrock.lang.bi.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab95"></a><h2 class="section">Powers in BIs</h2>
+<a id="lab96"></a><h2 class="section">Powers in BIs</h2>
 
 <div class="paragraph"> </div>
 
@@ -387,9 +387,9 @@ <h1 class="libtitle">bedrock.lang.bi.big_op</h1>
 </div>
 
 <div class="doc">
-<a id="lab96"></a><h1 class="section">Avoid exotic goals like <span class="inlinecode"><span class="id" title="class">Timeless</span></span> <span class="inlinecode"><span class="id" title="var">emp</span></span>, <span class="inlinecode"><span class="id" title="class">Affine</span></span> <span class="inlinecode"><span class="id" title="var">True</span></span> when <span class="inlinecode"><span class="id" title="var">n</span></span> a</h1>
+<a id="lab97"></a><h1 class="section">Avoid exotic goals like <span class="inlinecode"><span class="id" title="class">Timeless</span></span> <span class="inlinecode"><span class="id" title="var">emp</span></span>, <span class="inlinecode"><span class="id" title="class">Affine</span></span> <span class="inlinecode"><span class="id" title="var">True</span></span> when <span class="inlinecode"><span class="id" title="var">n</span></span> a</h1>
 
-<a id="lab97"></a><h1 class="section">non-zero constructor.</h1>
+<a id="lab98"></a><h1 class="section">non-zero constructor.</h1>
 
 
 </div>

docs/_static/coqdoc/bedrock.lang.bi.embedding.html

@@ -50,7 +50,7 @@ <h1 class="libtitle">bedrock.lang.bi.embedding</h1>
 </div>
 
 <div class="doc">
-<a id="lab86"></a><h1 class="section">Composing embeddings</h1>
+<a id="lab87"></a><h1 class="section">Composing embeddings</h1>
  Given embeddings <span class="inlinecode"><span class="id" title="class">Embed</span></span> <span class="inlinecode"><span class="id" title="var">PROP1</span></span> <span class="inlinecode"><span class="id" title="var">PROP2</span></span> and <span class="inlinecode"><span class="id" title="class">Embed</span></span> <span class="inlinecode"><span class="id" title="var">PROP2</span></span> <span class="inlinecode"><span class="id" title="var">PROP3</span></span>,
 <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.embedding.html#compose_embed"><span class="id" title="definition">compose_embed</span></a></span> <span class="inlinecode"><span class="id" title="var">PROP2</span></span> is the induced embedding <span class="inlinecode"><span class="id" title="class">Embed</span></span> <span class="inlinecode"><span class="id" title="var">PROP1</span></span> <span class="inlinecode"><span class="id" title="var">PROP3</span></span>.
 Its <span class="inlinecode"><span class="id" title="class">BiEmbed</span></span>, etc instances are available after <span class="inlinecode"><span class="id" title="keyword">Import</span></span>

docs/_static/coqdoc/bedrock.lang.bi.entailsN.html

@@ -52,7 +52,7 @@ <h1 class="libtitle">bedrock.lang.bi.entailsN</h1>
 </div>
 
 <div class="doc">
-<a id="lab75"></a><h1 class="section">Step-indexed entailment</h1>
+<a id="lab76"></a><h1 class="section">Step-indexed entailment</h1>
  We axiomatize a generalization <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">⊢{<span class="id" title="var">n</span>}</span> <span class="inlinecode"><span class="id" title="var">Q</span></span> of Iris entailment that
 satisfies
 

docs/_static/coqdoc/bedrock.lang.bi.fractional.html

@@ -54,7 +54,7 @@ <h1 class="libtitle">bedrock.lang.bi.fractional</h1>
 </div>
 
 <div class="doc">
-<a id="lab85"></a><h1 class="section">Simple extensions to iris.bi.lib.fractional</h1>
+<a id="lab86"></a><h1 class="section">Simple extensions to iris.bi.lib.fractional</h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.invariants.html

@@ -199,7 +199,7 @@ <h1 class="libtitle">bedrock.lang.bi.invariants</h1>
 </div>
 
 <div class="doc">
-<a id="lab88"></a><h2 class="section">Proof mode integration</h2>
+<a id="lab89"></a><h2 class="section">Proof mode integration</h2>
 
 </div>
 <div class="code">
@@ -220,7 +220,7 @@ <h1 class="libtitle">bedrock.lang.bi.invariants</h1>
 </div>
 
 <div class="doc">
-<a id="lab89"></a><h2 class="section">Derived properties</h2>
+<a id="lab90"></a><h2 class="section">Derived properties</h2>
 
 </div>
 <div class="code">

docs/_static/coqdoc/bedrock.lang.bi.linearity.html

@@ -187,7 +187,7 @@ <h1 class="libtitle">bedrock.lang.bi.linearity</h1>
 </div>
 
 <div class="doc">
-<a id="lab92"></a><h3 class="section">Other instances that we derive from affinity but seem safe.</h3>
+<a id="lab93"></a><h3 class="section">Other instances that we derive from affinity but seem safe.</h3>
 
 </div>
 <div class="code">
@@ -213,7 +213,7 @@ <h1 class="libtitle">bedrock.lang.bi.linearity</h1>
 </div>
 
 <div class="doc">
-<a id="lab93"></a><h3 class="section">Lift over <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.monpred_own.html#monPred"><span class="id" title="abbreviation">monPred</span></a></span> instances declared above.</h3>
+<a id="lab94"></a><h3 class="section">Lift over <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.monpred_own.html#monPred"><span class="id" title="abbreviation">monPred</span></a></span> instances declared above.</h3>
 
 </div>
 <div class="code">

docs/_static/coqdoc/bedrock.lang.bi.monpred.html

@@ -99,7 +99,7 @@ <h1 class="libtitle">bedrock.lang.bi.monpred</h1>
 </div>
 
 <div class="doc">
-<a id="lab87"></a><h2 class="section">Discrete BI indices and discrete BI index elements</h2>
+<a id="lab88"></a><h2 class="section">Discrete BI indices and discrete BI index elements</h2>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.observe.html

@@ -52,7 +52,7 @@ <h1 class="libtitle">bedrock.lang.bi.observe</h1>
 </div>
 
 <div class="doc">
-<a id="lab77"></a><h1 class="section">Observations</h1>
+<a id="lab78"></a><h1 class="section">Observations</h1>
  We define type classes for making observations and a few instances
 lifting those observations through the logic. Additional instances are
 defined elsewhere. 

docs/_static/coqdoc/bedrock.lang.bi.only_provable.html

@@ -93,7 +93,7 @@ <h1 class="libtitle">bedrock.lang.bi.only_provable</h1>
 </div>
 
 <div class="doc">
-<a id="lab78"></a><h1 class="section">Properties of <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.only_provable.html#only_provable"><span class="id" title="module">only_provable</span></a></span>.</h1>
+<a id="lab79"></a><h1 class="section">Properties of <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.only_provable.html#only_provable"><span class="id" title="module">only_provable</span></a></span>.</h1>
 
 </div>
 <div class="code">
@@ -333,20 +333,20 @@ <h1 class="libtitle">bedrock.lang.bi.only_provable</h1>
 </div>
 
 <div class="doc">
-<a id="lab79"></a><h1 class="section">We don't register instances</h1>
+<a id="lab80"></a><h1 class="section">We don't register instances</h1>
 
    *
-<a id="lab80"></a><h1 class="section">- <span class="inlinecode">@<span class="id" title="var">FromAffinely</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.iprop_own.html#PROP"><span class="id" title="abbreviation">PROP</span></a></span> <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span> <span class="inlinecode">⌜<a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a>⌝</span></h1>
+<a id="lab81"></a><h1 class="section">- <span class="inlinecode">@<span class="id" title="var">FromAffinely</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.iprop_own.html#PROP"><span class="id" title="abbreviation">PROP</span></a></span> <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span> <span class="inlinecode">⌜<a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a>⌝</span></h1>
 
    *
-<a id="lab81"></a><h1 class="section">- <span class="inlinecode">@<span class="id" title="var">IntoAbsorbingly</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.iprop_own.html#PROP"><span class="id" title="abbreviation">PROP</span></a></span> <span class="inlinecode">⌜<a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a>⌝</span> <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span></h1>
+<a id="lab82"></a><h1 class="section">- <span class="inlinecode">@<span class="id" title="var">IntoAbsorbingly</span></span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.logic.iprop_own.html#PROP"><span class="id" title="abbreviation">PROP</span></a></span> <span class="inlinecode">⌜<a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a>⌝</span> <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span></h1>
 
    *
-<a id="lab82"></a><h1 class="section">as they would interact poorly with, e.g., <span class="inlinecode"><span class="id" title="var">iSplit</span></span>, changing</h1>
+<a id="lab83"></a><h1 class="section">as they would interact poorly with, e.g., <span class="inlinecode"><span class="id" title="var">iSplit</span></span>, changing</h1>
 
-<a id="lab83"></a><h1 class="section">goals like <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span> <span class="inlinecode">**</span> <span class="inlinecode"><span class="id" title="var">Q</span></span> into subgoals involving <span class="inlinecode"><span class="id" title="projection">bi_pure</span></span></h1>
+<a id="lab84"></a><h1 class="section">goals like <span class="inlinecode">[|</span> <span class="inlinecode"><a class="idref" href="bedrock.lang.cpp.syntax.types.html#type_ind'.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode">|]</span> <span class="inlinecode">**</span> <span class="inlinecode"><span class="id" title="var">Q</span></span> into subgoals involving <span class="inlinecode"><span class="id" title="projection">bi_pure</span></span></h1>
 
-<a id="lab84"></a><h1 class="section">rather than <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.only_provable.html#only_provable"><span class="id" title="module">only_provable</span></a></span>.</h1>
+<a id="lab85"></a><h1 class="section">rather than <span class="inlinecode"><a class="idref" href="bedrock.lang.bi.only_provable.html#only_provable"><span class="id" title="module">only_provable</span></a></span>.</h1>
 
 
 </div>

docs/_static/coqdoc/bedrock.lang.bi.prelude.html

@@ -72,7 +72,7 @@ <h1 class="libtitle">bedrock.lang.bi.prelude</h1>
 </div>
 
 <div class="doc">
-<a id="lab90"></a><h1 class="section">Notation for functions in the Iris scope. To upstream,</h1>
+<a id="lab91"></a><h1 class="section">Notation for functions in the Iris scope. To upstream,</h1>
 
 per https://gitlab.mpi-sws.org/iris/iris/-/issues/320. 
 </div>
@@ -172,7 +172,7 @@ <h1 class="libtitle">bedrock.lang.bi.prelude</h1>
 </div>
 
 <div class="doc">
-<a id="lab91"></a><h2 class="section">Big op notation</h2>
+<a id="lab92"></a><h2 class="section">Big op notation</h2>
 
 </div>
 <div class="code">

docs/_static/coqdoc/bedrock.lang.bi.spec.constant.html

@@ -56,7 +56,7 @@ <h1 class="libtitle">bedrock.lang.bi.spec.constant</h1>
 </div>
 
 <div class="doc">
-<a id="lab119"></a><h1 class="section">Spec building block: logical constants</h1>
+<a id="lab120"></a><h1 class="section">Spec building block: logical constants</h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.spec.contender_token.html

@@ -58,7 +58,7 @@ <h1 class="libtitle">bedrock.lang.bi.spec.contender_token</h1>
 </div>
 
 <div class="doc">
-<a id="lab120"></a><h1 class="section">Spec building block: Contender tokens</h1>
+<a id="lab121"></a><h1 class="section">Spec building block: Contender tokens</h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.spec.exclusive.html

@@ -56,7 +56,7 @@ <h1 class="libtitle">bedrock.lang.bi.spec.exclusive</h1>
 </div>
 
 <div class="doc">
-<a id="lab121"></a><h1 class="section">Spec building block: Exclusive tokens</h1>
+<a id="lab122"></a><h1 class="section">Spec building block: Exclusive tokens</h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.spec.frac_splittable.html

@@ -60,7 +60,7 @@ <h1 class="libtitle">bedrock.lang.bi.spec.frac_splittable</h1>
 </div>
 
 <div class="doc">
-<a id="lab122"></a><h1 class="section">Spec building block: fractional ownership</h1>
+<a id="lab123"></a><h1 class="section">Spec building block: fractional ownership</h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.split_andb.html

@@ -52,7 +52,7 @@ <h1 class="libtitle">bedrock.lang.bi.split_andb</h1>
 </div>
 
 <div class="doc">
-<a id="lab98"></a><h1 class="section">Splitting and combining booleans on <span class="inlinecode">&amp;&amp;</span></h1>
+<a id="lab99"></a><h1 class="section">Splitting and combining booleans on <span class="inlinecode">&amp;&amp;</span></h1>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.bi.split_frac.html

@@ -55,7 +55,7 @@ <h1 class="libtitle">bedrock.lang.bi.split_frac</h1>
 </div>
 
 <div class="doc">
-<a id="lab99"></a><h1 class="section">Splitting and combining fractions</h1>
+<a id="lab100"></a><h1 class="section">Splitting and combining fractions</h1>
 
 <div class="paragraph"> </div>
 
@@ -115,7 +115,7 @@ <h1 class="libtitle">bedrock.lang.bi.split_frac</h1>
 </div>
 
 <div class="doc">
-<a id="lab100"></a><h2 class="section">Operations on fractions</h2>
+<a id="lab101"></a><h2 class="section">Operations on fractions</h2>
 
 </div>
 <div class="code">
@@ -343,7 +343,7 @@ <h1 class="libtitle">bedrock.lang.bi.split_frac</h1>
 </div>
 
 <div class="doc">
-<a id="lab101"></a><h2 class="section">Splitting fractions</h2>
+<a id="lab102"></a><h2 class="section">Splitting fractions</h2>
 
 <div class="paragraph"> </div>
 
@@ -514,7 +514,7 @@ <h1 class="libtitle">bedrock.lang.bi.split_frac</h1>
 </div>
 
 <div class="doc">
-<a id="lab102"></a><h2 class="section">Combining fractions</h2>
+<a id="lab103"></a><h2 class="section">Combining fractions</h2>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.cpp.algebra.cfrac.html

@@ -57,7 +57,7 @@ <h1 class="libtitle">bedrock.lang.cpp.algebra.cfrac</h1>
 </div>
 
 <div class="doc">
-<a id="lab71"></a><h1 class="section">Const/mutable fractions</h1>
+<a id="lab72"></a><h1 class="section">Const/mutable fractions</h1>
 
 <div class="paragraph"> </div>
 
@@ -276,7 +276,7 @@ <h1 class="libtitle">bedrock.lang.cpp.algebra.cfrac</h1>
 </div>
 
 <div class="doc">
-<a id="lab72"></a><h2 class="section">OFE</h2>
+<a id="lab73"></a><h2 class="section">OFE</h2>
 
 </div>
 <div class="code">
@@ -315,7 +315,7 @@ <h1 class="libtitle">bedrock.lang.cpp.algebra.cfrac</h1>
 </div>
 
 <div class="doc">
-<a id="lab73"></a><h2 class="section">CMRA</h2>
+<a id="lab74"></a><h2 class="section">CMRA</h2>
 
 </div>
 <div class="code">
@@ -420,7 +420,7 @@ <h1 class="libtitle">bedrock.lang.cpp.algebra.cfrac</h1>
 </div>
 
 <div class="doc">
-<a id="lab74"></a><h2 class="section">Backwards compatibility</h2>
+<a id="lab75"></a><h2 class="section">Backwards compatibility</h2>
 
 <div class="paragraph"> </div>
 

docs/_static/coqdoc/bedrock.lang.cpp.arith.operator.html

@@ -48,7 +48,7 @@ <h1 class="libtitle">bedrock.lang.cpp.arith.operator</h1>
 </div>
 
 <div class="doc">
-<a id="lab123"></a><h1 class="section">Semantics of arithmetic and pointer operators: support operators.</h1>
+<a id="lab124"></a><h1 class="section">Semantics of arithmetic and pointer operators: support operators.</h1>
 
 
 </div>