Skip to content

Commit 52748af

Browse files
github-actions[bot]github-actions[bot]
committed
Update formal specification documentation
- Updated from ouroboros-leios-formal-spec repository - Run ID: 17245612895 - Triggered by: repository_dispatch
1 parent 3459d47 commit 52748af

File tree

549 files changed

+722
-1229
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

549 files changed

+722
-1229
lines changed

‎site/static/formal-spec/Agda.Builtin.Bool.html‎

Lines changed: 1 addition & 1 deletion
Large diffs are not rendered by default.

‎site/static/formal-spec/Agda.Builtin.Char.Properties.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
<path fill="currentColor" d="M9.37,5.51C9.19,6.15,9.1,6.82,9.1,7.5c0,4.08,3.32,7.4,7.4,7.4c0.68,0,1.35-0.09,1.99-0.27C17.45,17.19,14.93,19,12,19 c-3.86,0-7-3.14-7-7C5,9.07,6.81,6.55,9.37,5.51z M12,3c-4.97,0-9,4.03-9,9s4.03,9,9,9s9-4.03,9-9c0-0.46-0.04-0.92-0.1-1.36 c-0.98,1.37-2.58,2.26-4.4,2.26c-2.98,0-5.4-2.42-5.4-5.4c0-1.81,0.89-3.42,2.26-4.4C12.92,3.04,12.46,3,12,3L12,3z"></path>
1818
</svg>
1919
</span>
20-
</button></div></header><div class="main-wrapper"><aside class="sidebar"><h3 class="modules-header">Modules</h3><h4 class="module-group-header">Leios</h4><ul class="module-list"><li class="module-item"><a href="Leios.Abstract.html" class="module-link">Abstract</a></li><li class="module-item"><a href="Leios.Base.html" class="module-link">Base</a></li><li class="module-item"><a href="Leios.Blocks.html" class="module-link">Blocks</a></li><li class="module-item"><a href="Leios.Config.html" class="module-link">Config</a></li><li class="module-item"><a href="Leios.Defaults.html" class="module-link">Defaults</a></li><li class="module-item"><a href="Leios.FFD.html" class="module-link">FFD</a></li><li class="module-item"><a href="Leios.Foreign.BaseTypes.html" class="module-link">Foreign.BaseTypes</a></li><li class="module-item"><a href="Leios.Foreign.HsTypes.html" class="module-link">Foreign.HsTypes</a></li><li class="module-item"><a href="Leios.Foreign.Types.html" class="module-link">Foreign.Types</a></li><li class="module-item"><a href="Leios.Foreign.Util.html" class="module-link">Foreign.Util</a></li><li class="module-item"><a href="Leios.KeyRegistration.html" class="module-link">KeyRegistration</a></li><li class="module-item"><a href="Leios.Prelude.html" class="module-link">Prelude</a></li><li class="module-item"><a href="Leios.Protocol.html" class="module-link">Protocol</a></li><li class="module-item"><a href="Leios.Short.html" class="module-link">Short</a></li><li class="module-item"><a href="Leios.Short.Trace.Verifier.html" class="module-link">Short.Trace.Verifier</a></li><li class="module-item"><a href="Leios.SpecStructure.html" class="module-link">SpecStructure</a></li><li class="module-item"><a href="Leios.Traces.html" class="module-link">Traces</a></li><li class="module-item"><a href="Leios.Voting.html" class="module-link">Voting</a></li><li class="module-item"><a href="Leios.VRF.html" class="module-link">VRF</a></li></ul><h4 class="module-group-header">Network</h4><ul class="module-list"><li class="module-item"><a href="Network.BasicBroadcast.html" class="module-link">BasicBroadcast</a></li><li class="module-item"><a href="Network.Leios.html" class="module-link">Leios</a></li></ul></aside><div class="main-content"><pre class="Agda has-copy-button" id="B1"><div class="code-container"><div class="line-numbers"><a href="#B1-L1" id="B1-L1" class="line-number" data-line-number="1" data-block-id="B1">1</a><a href="#B1-L2" id="B1-L2" class="line-number" data-line-number="2" data-block-id="B1">2</a><a href="#B1-L3" id="B1-L3" class="line-number" data-line-number="3" data-block-id="B1">3</a><a href="#B1-L4" id="B1-L4" class="line-number" data-line-number="4" data-block-id="B1">4</a><a href="#B1-L5" id="B1-L5" class="line-number" data-line-number="5" data-block-id="B1">5</a><a href="#B1-L6" id="B1-L6" class="line-number" data-line-number="6" data-block-id="B1">6</a><a href="#B1-L7" id="B1-L7" class="line-number" data-line-number="7" data-block-id="B1">7</a><a href="#B1-L8" id="B1-L8" class="line-number" data-line-number="8" data-block-id="B1">8</a><a href="#B1-L9" id="B1-L9" class="line-number" data-line-number="9" data-block-id="B1">9</a><a href="#B1-L10" id="B1-L10" class="line-number" data-line-number="10" data-block-id="B1">10</a></div><div class="code-content"><div id="B1-LC1" class="code-line"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Pragma">--level-universe</a> <a id="92" class="Symbol">#-}</a></div><div id="B1-LC2" class="code-line">&nbsp;</div><div id="B1-LC3" class="code-line"><a id="97" class="Keyword">module</a> <a id="104" href="Agda.Builtin.Char.Properties.html" class="Module">Agda.Builtin.Char.Properties</a> <a id="133" class="Keyword">where</a></div><div id="B1-LC4" class="code-line">&nbsp;</div><div id="B1-LC5" class="code-line"><a id="140" class="Keyword">open</a> <a id="145" class="Keyword">import</a> <a id="152" href="Agda.Builtin.Char.html" class="Module">Agda.Builtin.Char</a></div><div id="B1-LC6" class="code-line"><a id="170" class="Keyword">open</a> <a id="175" class="Keyword">import</a> <a id="182" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a></div><div id="B1-LC7" class="code-line">&nbsp;</div><div id="B1-LC8" class="code-line"><a id="205" class="Keyword">primitive</a></div><div id="B1-LC9" class="code-line">&nbsp;</div><div id="B1-LC10" class="code-line"> <a id="primCharToNatInjective"></a><a id="218" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#218" data-hoverable="true" data-position="218" data-target-file="Agda.Builtin.Char.Properties.html">primCharToNatInjective</a> <a id="241" class="Symbol">:</a> <a id="243" class="Symbol">∀</a> <a id="245" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="247" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a> <a id="249" class="Symbol">→</a> <a id="251" href="Agda.Builtin.Char.html#B1-L16" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.html#448" data-hoverable="true" data-position="448" data-target-file="Agda.Builtin.Char.html">primCharToNat</a> <a id="265" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="267" href="Agda.Builtin.Equality.html#B1-L6" class="Datatype Operator type-hoverable" data-original-href="Agda.Builtin.Equality.html#150" data-hoverable="true" data-position="150" data-target-file="Agda.Builtin.Equality.html">≡</a> <a id="269" href="Agda.Builtin.Char.html#B1-L16" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.html#448" data-hoverable="true" data-position="448" data-target-file="Agda.Builtin.Char.html">primCharToNat</a> <a id="283" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a> <a id="285" class="Symbol">→</a> <a id="287" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="289" href="Agda.Builtin.Equality.html#B1-L6" class="Datatype Operator type-hoverable" data-original-href="Agda.Builtin.Equality.html#150" data-hoverable="true" data-position="150" data-target-file="Agda.Builtin.Equality.html">≡</a> <a id="291" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a></div></div></div><button class="copy-code-button" title="Copy code">
20+
</button></div></header><div class="main-wrapper"><aside class="sidebar"><h3 class="modules-header">Modules</h3><h4 class="module-group-header">Leios</h4><ul class="module-list"><li class="module-item"><a href="Leios.Abstract.html" class="module-link">Abstract</a></li><li class="module-item"><a href="Leios.Base.html" class="module-link">Base</a></li><li class="module-item"><a href="Leios.Blocks.html" class="module-link">Blocks</a></li><li class="module-item"><a href="Leios.Config.html" class="module-link">Config</a></li><li class="module-item"><a href="Leios.Defaults.html" class="module-link">Defaults</a></li><li class="module-item"><a href="Leios.FFD.html" class="module-link">FFD</a></li><li class="module-item"><a href="Leios.Foreign.BaseTypes.html" class="module-link">Foreign.BaseTypes</a></li><li class="module-item"><a href="Leios.Foreign.HsTypes.html" class="module-link">Foreign.HsTypes</a></li><li class="module-item"><a href="Leios.Foreign.Types.html" class="module-link">Foreign.Types</a></li><li class="module-item"><a href="Leios.Foreign.Util.html" class="module-link">Foreign.Util</a></li><li class="module-item"><a href="Leios.KeyRegistration.html" class="module-link">KeyRegistration</a></li><li class="module-item"><a href="Leios.Prelude.html" class="module-link">Prelude</a></li><li class="module-item"><a href="Leios.Protocol.html" class="module-link">Protocol</a></li><li class="module-item"><a href="Leios.Short.html" class="module-link">Short</a></li><li class="module-item"><a href="Leios.SpecStructure.html" class="module-link">SpecStructure</a></li><li class="module-item"><a href="Leios.Traces.html" class="module-link">Traces</a></li><li class="module-item"><a href="Leios.Voting.html" class="module-link">Voting</a></li><li class="module-item"><a href="Leios.VRF.html" class="module-link">VRF</a></li></ul><h4 class="module-group-header">Network</h4><ul class="module-list"><li class="module-item"><a href="Network.BasicBroadcast.html" class="module-link">BasicBroadcast</a></li></ul></aside><div class="main-content"><pre class="Agda has-copy-button" id="B1"><div class="code-container"><div class="line-numbers"><a href="#B1-L1" id="B1-L1" class="line-number" data-line-number="1" data-block-id="B1">1</a><a href="#B1-L2" id="B1-L2" class="line-number" data-line-number="2" data-block-id="B1">2</a><a href="#B1-L3" id="B1-L3" class="line-number" data-line-number="3" data-block-id="B1">3</a><a href="#B1-L4" id="B1-L4" class="line-number" data-line-number="4" data-block-id="B1">4</a><a href="#B1-L5" id="B1-L5" class="line-number" data-line-number="5" data-block-id="B1">5</a><a href="#B1-L6" id="B1-L6" class="line-number" data-line-number="6" data-block-id="B1">6</a><a href="#B1-L7" id="B1-L7" class="line-number" data-line-number="7" data-block-id="B1">7</a><a href="#B1-L8" id="B1-L8" class="line-number" data-line-number="8" data-block-id="B1">8</a><a href="#B1-L9" id="B1-L9" class="line-number" data-line-number="9" data-block-id="B1">9</a><a href="#B1-L10" id="B1-L10" class="line-number" data-line-number="10" data-block-id="B1">10</a></div><div class="code-content"><div id="B1-LC1" class="code-line"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical-compatible</a> <a id="34" class="Pragma">--safe</a> <a id="41" class="Pragma">--no-sized-types</a> <a id="58" class="Pragma">--no-guardedness</a> <a id="75" class="Pragma">--level-universe</a> <a id="92" class="Symbol">#-}</a></div><div id="B1-LC2" class="code-line">&nbsp;</div><div id="B1-LC3" class="code-line"><a id="97" class="Keyword">module</a> <a id="104" href="Agda.Builtin.Char.Properties.html" class="Module">Agda.Builtin.Char.Properties</a> <a id="133" class="Keyword">where</a></div><div id="B1-LC4" class="code-line">&nbsp;</div><div id="B1-LC5" class="code-line"><a id="140" class="Keyword">open</a> <a id="145" class="Keyword">import</a> <a id="152" href="Agda.Builtin.Char.html" class="Module">Agda.Builtin.Char</a></div><div id="B1-LC6" class="code-line"><a id="170" class="Keyword">open</a> <a id="175" class="Keyword">import</a> <a id="182" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a></div><div id="B1-LC7" class="code-line">&nbsp;</div><div id="B1-LC8" class="code-line"><a id="205" class="Keyword">primitive</a></div><div id="B1-LC9" class="code-line">&nbsp;</div><div id="B1-LC10" class="code-line"> <a id="primCharToNatInjective"></a><a id="218" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#218" data-hoverable="true" data-position="218" data-target-file="Agda.Builtin.Char.Properties.html">primCharToNatInjective</a> <a id="241" class="Symbol">:</a> <a id="243" class="Symbol">∀</a> <a id="245" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="247" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a> <a id="249" class="Symbol">→</a> <a id="251" href="Agda.Builtin.Char.html#B1-L16" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.html#448" data-hoverable="true" data-position="448" data-target-file="Agda.Builtin.Char.html">primCharToNat</a> <a id="265" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="267" href="Agda.Builtin.Equality.html#B1-L6" class="Datatype Operator type-hoverable" data-original-href="Agda.Builtin.Equality.html#150" data-hoverable="true" data-position="150" data-target-file="Agda.Builtin.Equality.html">≡</a> <a id="269" href="Agda.Builtin.Char.html#B1-L16" class="Primitive type-hoverable" data-original-href="Agda.Builtin.Char.html#448" data-hoverable="true" data-position="448" data-target-file="Agda.Builtin.Char.html">primCharToNat</a> <a id="283" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a> <a id="285" class="Symbol">→</a> <a id="287" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#245" data-hoverable="true" data-position="245" data-target-file="Agda.Builtin.Char.Properties.html">a</a> <a id="289" href="Agda.Builtin.Equality.html#B1-L6" class="Datatype Operator type-hoverable" data-original-href="Agda.Builtin.Equality.html#150" data-hoverable="true" data-position="150" data-target-file="Agda.Builtin.Equality.html">≡</a> <a id="291" href="Agda.Builtin.Char.Properties.html#B1-L10" class="Bound type-hoverable" data-original-href="Agda.Builtin.Char.Properties.html#247" data-hoverable="true" data-position="247" data-target-file="Agda.Builtin.Char.Properties.html">b</a></div></div></div><button class="copy-code-button" title="Copy code">
2121
<svg width="16" height="16" viewBox="0 0 16 16">
2222
<path fill="currentColor" d="M0 6.75C0 5.784.784 5 1.75 5h1.5a.75.75 0 0 1 0 1.5h-1.5a.25.25 0 0 0-.25.25v7.5c0 .138.112.25.25.25h7.5a.25.25 0 0 0 .25-.25v-1.5a.75.75 0 0 1 1.5 0v1.5A1.75 1.75 0 0 1 9.25 16h-7.5A1.75 1.75 0 0 1 0 14.25Z"></path><path fill="currentColor" d="M5 1.75C5 .784 5.784 0 6.75 0h7.5C15.216 0 16 .784 16 1.75v7.5A1.75 1.75 0 0 1 14.25 11h-7.5A1.75 1.75 0 0 1 5 9.25Zm1.75-.25a.25.25 0 0 0-.25.25v7.5c0 .138.112.25.25.25h7.5a.25.25 0 0 0 .25-.25v-7.5a.25.25 0 0 0-.25-.25Z"></path>
2323
</svg>

0 commit comments

Comments
 (0)