Skip to content

Commit

Permalink
[github pages] BRiCk documentation created from 0ec27097
Browse files Browse the repository at this point in the history
  • Loading branch information
project_18556810_bot committed Dec 4, 2024
1 parent 16cbd04 commit d945203
Show file tree
Hide file tree
Showing 8 changed files with 31 additions and 31 deletions.
36 changes: 18 additions & 18 deletions docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.bi.telescopes.html
View file

Large diffs are not rendered by default.

8 changes: 4 additions & 4 deletions docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.mtraverse.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,9 +94,9 @@ <h1 class="libtitle">bedrock.lang.cpp.syntax.mtraverse</h1>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> {<a id="option.F" class="idref" href="#option.F"><span class="id" title="variable">F</span></a> : <span class="id" title="var">Type@</span>{<span class="id" title="var">u1</span>} <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">Type@</span>{<span class="id" title="var">u2</span>}}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">FMap@</span><span class="id" title="class">{</span><span class="id" title="class">u1</span> <span class="id" title="class">u2</span> <span class="id" title="class">uB</span><span class="id" title="class">}</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">FMap@</span>{<span class="id" title="var">u1</span> <span class="id" title="var">u2</span> <span class="id" title="var">uB</span>} <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">MRet</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>, !<span class="id" title="abbreviation">MFail</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{<a id="option.AP" class="idref" href="#option.AP"><span class="id" title="variable">AP</span></a> : !<span class="id" title="class">Ap@</span><span class="id" title="class">{</span><span class="id" title="class">u1</span> <span class="id" title="class">u2</span> <span class="id" title="class">uA</span> <span class="id" title="class">uB</span><span class="id" title="class">}</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{<a id="option.AP" class="idref" href="#option.AP"><span class="id" title="variable">AP</span></a> : !<span class="id" title="class">Ap@</span>{<span class="id" title="var">u1</span> <span class="id" title="var">u2</span> <span class="id" title="var">uA</span> <span class="id" title="var">uB</span>} <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#option.F"><span class="id" title="variable">F</span></a>}.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="option_traverse2" class="idref" href="#option_traverse2"><span class="id" title="definition">option_traverse2@</span></a>{<span class="id" title="var">uC</span> | <span class="id" title="var">uC</span> &lt;= <span class="id" title="var">uA</span> , <span class="id" title="var">uC</span> &lt;= <span class="id" title="var">uB</span>}<br/>
Expand Down Expand Up @@ -127,9 +127,9 @@ <h1 class="libtitle">bedrock.lang.cpp.syntax.mtraverse</h1>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> {<a id="list.F" class="idref" href="#list.F"><span class="id" title="variable">F</span></a> : <span class="id" title="var">Type@</span>{<span class="id" title="var">u1</span>} <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">Type@</span>{<span class="id" title="var">u2</span>}}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">FMap@</span><span class="id" title="class">{</span><span class="id" title="class">u1</span> <span class="id" title="class">u2</span> <span class="id" title="class">uB</span><span class="id" title="class">}</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">FMap@</span>{<span class="id" title="var">u1</span> <span class="id" title="var">u2</span> <span class="id" title="var">uB</span>} <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{!<span class="id" title="class">MRet</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>, !<span class="id" title="abbreviation">MFail</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{<a id="list.AP" class="idref" href="#list.AP"><span class="id" title="variable">AP</span></a> : !<span class="id" title="class">Ap@</span><span class="id" title="class">{</span><span class="id" title="class">u1</span> <span class="id" title="class">u2</span> <span class="id" title="class">uA</span> <span class="id" title="class">uB</span><span class="id" title="class">}</span> <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>}.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Context</span> `{<a id="list.AP" class="idref" href="#list.AP"><span class="id" title="variable">AP</span></a> : !<span class="id" title="class">Ap@</span>{<span class="id" title="var">u1</span> <span class="id" title="var">u2</span> <span class="id" title="var">uA</span> <span class="id" title="var">uB</span>} <a class="idref" href="bedrock.lang.cpp.syntax.mtraverse.html#list.F"><span class="id" title="variable">F</span></a>}.<br/>

<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="list_traverse2" class="idref" href="#list_traverse2"><span class="id" title="definition">list_traverse2@</span></a>{<span class="id" title="var">uC</span> | <span class="id" title="var">uC</span> &lt;= <span class="id" title="var">uA</span> , <span class="id" title="var">uC</span> &lt;= <span class="id" title="var">uB</span>}<br/>
Expand Down
2 changes: 1 addition & 1 deletion docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.name_notation.parser.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ <h1 class="libtitle">bedrock.lang.cpp.syntax.name_notation.parser</h1>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Context</span> {<a id="parser.with_M.RET" class="idref" href="#parser.with_M.RET"><span class="id" title="variable">RET</span></a> : <span class="id" title="class">MRet</span> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>} {<a id="parser.with_M.FMAP" class="idref" href="#parser.with_M.FMAP"><span class="id" title="variable">FMAP</span></a> : <span class="id" title="class">FMap</span> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>} {<a id="parser.with_M.AP" class="idref" href="#parser.with_M.AP"><span class="id" title="variable">AP</span></a> : <span class="id" title="class">Ap</span> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>} {<a id="parser.with_M.MBIND" class="idref" href="#parser.with_M.MBIND"><span class="id" title="variable">MBIND</span></a> : <span class="id" title="class">MBind</span> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>}.<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="parser.M" class="idref" href="#parser.M"><span class="id" title="abbreviation">M</span></a> := (<span class="id" title="definition">parsec.M@</span><span class="id" title="definition">{</span><span class="id" title="definition">Set</span> <span class="id" title="definition">_</span> <span class="id" title="definition">_</span> <span class="id" title="definition">_</span> <span class="id" title="definition">_</span> <span class="id" title="definition">_</span> <span class="id" title="definition">_</span><span class="id" title="definition">}</span> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Byte.html#byte"><span class="id" title="inductive">Byte.byte</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="parser.M" class="idref" href="#parser.M"><span class="id" title="abbreviation">M</span></a> := (<span class="id" title="definition">parsec.M@</span>{<span class="id" title="keyword">Set</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span>} <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Byte.html#byte"><span class="id" title="inductive">Byte.byte</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.name_notation.parser.html#parser.with_M.Mbase"><span class="id" title="variable">Mbase</span></a>).<br/>

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="parser.digit_char" class="idref" href="#parser.digit_char"><span class="id" title="definition">digit_char</span></a> (<a id="b:8" class="idref" href="#b:8"><span class="id" title="binder">b</span></a> : <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Byte.html#byte"><span class="id" title="inductive">Byte.byte</span></a>) : <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
Expand Down
2 changes: 1 addition & 1 deletion docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.syntax.preliminary.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -952,7 +952,7 @@ <h1 class="libtitle">bedrock.lang.cpp.syntax.preliminary</h1>
<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;don't&nbsp;use&nbsp;the&nbsp;notation?&nbsp;*)</span><br/>
&nbsp;&nbsp;#[<span class="id" title="var">universes</span>(<span class="id" title="var">polymorphic</span>)]<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="MethodRef.traverse" class="idref" href="#MethodRef.traverse"><span class="id" title="definition">traverse@</span></a>{<span class="id" title="var">u</span> | } {<a id="F:201" class="idref" href="#F:201"><span class="id" title="binder">F</span></a> : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">Type@</span>{<span class="id" title="var">u</span>}} `{<a id="FM:202" class="idref" href="#FM:202"><span class="id" title="binder">FM</span></a>: <span class="id" title="class">FMap</span> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a>, <a id="AP:203" class="idref" href="#AP:203"><span class="id" title="binder">AP</span></a> : !<span class="id" title="class">Ap@</span><span class="id" title="class">{</span><span class="id" title="class">Set</span> <span class="id" title="class">u</span> <span class="id" title="class">Set</span> <span class="id" title="class">Set</span><span class="id" title="class">}</span> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a>}<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a id="MethodRef.traverse" class="idref" href="#MethodRef.traverse"><span class="id" title="definition">traverse@</span></a>{<span class="id" title="var">u</span> | } {<a id="F:201" class="idref" href="#F:201"><span class="id" title="binder">F</span></a> : <span class="id" title="keyword">Set</span> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">Type@</span>{<span class="id" title="var">u</span>}} `{<a id="FM:202" class="idref" href="#FM:202"><span class="id" title="binder">FM</span></a>: <span class="id" title="class">FMap</span> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a>, <a id="AP:203" class="idref" href="#AP:203"><span class="id" title="binder">AP</span></a> : !<span class="id" title="class">Ap@</span>{<span class="id" title="keyword">Set</span> <span class="id" title="var">u</span> <span class="id" title="keyword">Set</span> <span class="id" title="keyword">Set</span>} <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a>}<br/>
&nbsp;&nbsp;{<a id="name:204" class="idref" href="#name:204"><span class="id" title="binder">name</span></a> <a id="name':205" class="idref" href="#name':205"><span class="id" title="binder">name'</span></a> <a id="functype:206" class="idref" href="#functype:206"><span class="id" title="binder">functype</span></a> <a id="functype':207" class="idref" href="#functype':207"><span class="id" title="binder">functype'</span></a> <a id="Expr:208" class="idref" href="#Expr:208"><span class="id" title="binder">Expr</span></a> <a id="Expr':209" class="idref" href="#Expr':209"><span class="id" title="binder">Expr'</span></a> : <span class="id" title="keyword">Set</span>}<br/>
&nbsp;&nbsp;(<a id="f:210" class="idref" href="#f:210"><span class="id" title="binder">f</span></a> : <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#name:204"><span class="id" title="variable">name</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#name':205"><span class="id" title="variable">name'</span></a>) (<a id="g:211" class="idref" href="#g:211"><span class="id" title="binder">g</span></a> : <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#functype:206"><span class="id" title="variable">functype</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#functype':207"><span class="id" title="variable">functype'</span></a>)<br/>
&nbsp;&nbsp;(<a id="h:212" class="idref" href="#h:212"><span class="id" title="binder">h</span></a> : <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#Expr:208"><span class="id" title="variable">Expr</span></a> <a class="idref" href="http://coq.inria.fr/doc/V9.0+alpha/stdlib//Stdlib.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#F:201"><span class="id" title="variable">F</span></a> <a class="idref" href="bedrock.lang.cpp.syntax.preliminary.html#Expr':209"><span class="id" title="variable">Expr'</span></a>)<br/>
Expand Down
Loading

0 comments on commit d945203

Please sign in to comment.