1+ <!DOCTYPE HTML>
2+ < html > < head > < meta charset ="utf-8 "> < title > Agda.Builtin.Bool</ title > < link rel ="stylesheet " href ="Agda.css ">
3+ < link rel ="stylesheet " href ="agda.css ">
4+ < link href ="https://fonts.googleapis.com/css2?family=Fira+Code:wght@400;500&display=swap " rel ="stylesheet "> </ head > < body >
5+ < div class ="agda-header ">
6+ < div class ="agda-header-left ">
7+ < a href ="/formal-spec/ "> Back</ a >
8+ < button class ="search-button " onclick ="toggleSearch() ">
9+ < svg viewBox ="0 0 24 24 " width ="24 " height ="24 ">
10+ < path fill ="currentColor " d ="M15.5 14h-.79l-.28-.27C15.41 12.59 16 11.11 16 9.5 16 5.91 13.09 3 9.5 3S3 5.91 3 9.5 5.91 16 9.5 16c1.61 0 3.09-.59 4.23-1.57l.27.28v.79l5 4.99L20.49 19l-4.99-5zm-6 0C7.01 14 5 11.99 5 9.5S7.01 5 9.5 5 14 7.01 14 9.5 11.99 14 9.5 14z "/>
11+ </ svg >
12+ Search...
13+ </ button >
14+ </ div >
15+ < div class ="agda-header-right ">
16+ < a href ="https://github.com/input-output-hk/ouroboros-leios-formal-spec " class ="github-link " target ="_blank " rel ="noopener noreferrer " title ="View on GitHub ">
17+ < svg viewBox ="0 0 24 24 " width ="24 " height ="24 ">
18+ < path fill ="currentColor " d ="M12 0c-6.626 0-12 5.373-12 12 0 5.302 3.438 9.8 8.207 11.387.599.111.793-.261.793-.577v-2.234c-3.338.726-4.033-1.416-4.033-1.416-.546-1.387-1.333-1.756-1.333-1.756-1.089-.745.083-.729.083-.729 1.205.084 1.839 1.237 1.839 1.237 1.07 1.834 2.807 1.304 3.492.997.107-.775.418-1.305.762-1.604-2.665-.305-5.467-1.334-5.467-5.931 0-1.311.469-2.381 1.236-3.221-.124-.303-.535-1.524.117-3.176 0 0 1.008-.322 3.301 1.23.957-.266 1.983-.399 3.003-.404 1.02.005 2.047.138 3.006.404 2.291-1.552 3.297-1.23 3.297-1.23.653 1.653.242 2.874.118 3.176.77.84 1.235 1.911 1.235 3.221 0 4.609-2.807 5.624-5.479 5.921.43.372.823 1.102.823 2.222v3.293c0 .319.192.694.801.576 4.765-1.589 8.199-6.086 8.199-11.386 0-6.627-5.373-12-12-12z "/>
19+ </ svg >
20+ </ a >
21+ < button class ="theme-toggle " onclick ="toggleTheme() " title ="Toggle theme ">
22+ < span class ="light-icon ">
23+ < svg viewBox ="0 0 24 24 " width ="24 " height ="24 ">
24+ < path fill ="currentColor " d ="M12,9c1.65,0,3,1.35,3,3s-1.35,3-3,3s-3-1.35-3-3S10.35,9,12,9 M12,7c-2.76,0-5,2.24-5,5s2.24,5,5,5s5-2.24,5-5 S14.76,7,12,7L12,7z M2,13l2,0c0.55,0,1-0.45,1-1s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S1.45,13,2,13z M20,13l2,0c0.55,0,1-0.45,1-1 s-0.45-1-1-1l-2,0c-0.55,0-1,0.45-1,1S19.45,13,20,13z M11,2v2c0,0.55,0.45,1,1,1s1-0.45,1-1V2c0-0.55-0.45-1-1-1S11,1.45,11,2z M11,20v2c0,0.55,0.45,1,1,1s1-0.45,1-1v-2c0-0.55-0.45-1-1-1C11.45,19,11,19.45,11,20z M5.99,4.58c-0.39-0.39-1.03-0.39-1.41,0 c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0s0.39-1.03,0-1.41L5.99,4.58z M18.36,16.95 c-0.39-0.39-1.03-0.39-1.41,0c-0.39,0.39-0.39,1.03,0,1.41l1.06,1.06c0.39,0.39,1.03,0.39,1.41,0c0.39-0.39,0.39-1.03,0-1.41 L18.36,16.95z M19.42,5.99c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06c-0.39,0.39-0.39,1.03,0,1.41 s1.03,0.39,1.41,0L19.42,5.99z M7.05,18.36c0.39-0.39,0.39-1.03,0-1.41c-0.39-0.39-1.03-0.39-1.41,0l-1.06,1.06 c-0.39,0.39-0.39,1.03,0,1.41s1.03,0.39,1.41,0L7.05,18.36z "> </ path >
25+ </ svg >
26+ </ span >
27+ < span class ="dark-icon ">
28+ < svg viewBox ="0 0 24 24 " width ="24 " height ="24 ">
29+ < 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 >
30+ </ svg >
31+ </ span >
32+ </ button >
33+ </ div >
34+ </ div >
35+ < div class ="search-overlay ">
36+ < div class ="search-modal ">
37+ < div class ="search-container ">
38+ < input type ="text " class ="search-input " placeholder ="Search modules... " />
39+ < div class ="search-results "> </ div >
40+ </ div >
41+ </ div >
42+ </ div >
43+ < div class ="agda-container ">
44+ < nav class ="agda-sidebar ">
45+ < h3 > Modules</ h3 >
46+
47+ < h4 > Leios</ h4 >
48+ < ul >
49+ < li > < a href ="/agda_html/Leios.Abstract.html " > Abstract</ a > </ li >
50+ < li > < a href ="/agda_html/Leios.Base.html " > Base</ a > </ li >
51+ < li > < a href ="/agda_html/Leios.Blocks.html " > Blocks</ a > </ li >
52+ < li > < a href ="/agda_html/Leios.Config.html " > Config</ a > </ li >
53+ < li > < a href ="/agda_html/Leios.Defaults.html " > Defaults</ a > </ li >
54+ < li > < a href ="/agda_html/Leios.FFD.html " > FFD</ a > </ li >
55+ < li > < a href ="/agda_html/Leios.Foreign.BaseTypes.html " > Foreign.BaseTypes</ a > </ li >
56+ < li > < a href ="/agda_html/Leios.Foreign.HsTypes.html " > Foreign.HsTypes</ a > </ li >
57+ < li > < a href ="/agda_html/Leios.Foreign.Types.html " > Foreign.Types</ a > </ li >
58+ < li > < a href ="/agda_html/Leios.Foreign.Util.html " > Foreign.Util</ a > </ li >
59+ < li > < a href ="/agda_html/Leios.KeyRegistration.html " > KeyRegistration</ a > </ li >
60+ < li > < a href ="/agda_html/Leios.Network.html " > Network</ a > </ li >
61+ < li > < a href ="/agda_html/Leios.Prelude.html " > Prelude</ a > </ li >
62+ < li > < a href ="/agda_html/Leios.Protocol.html " > Protocol</ a > </ li >
63+ < li > < a href ="/agda_html/Leios.Short.html " > Short</ a > </ li >
64+ < li > < a href ="/agda_html/Leios.Short.Decidable.html " > Short.Decidable</ a > </ li >
65+ < li > < a href ="/agda_html/Leios.Short.Trace.Verifier.html " > Short.Trace.Verifier</ a > </ li >
66+ < li > < a href ="/agda_html/Leios.Short.Trace.Verifier.Test.html " > Short.Trace.Verifier.Test</ a > </ li >
67+ < li > < a href ="/agda_html/Leios.Simplified.html " > Simplified</ a > </ li >
68+ < li > < a href ="/agda_html/Leios.Simplified.Deterministic.html " > Simplified.Deterministic</ a > </ li >
69+ < li > < a href ="/agda_html/Leios.SpecStructure.html " > SpecStructure</ a > </ li >
70+ < li > < a href ="/agda_html/Leios.Traces.html " > Traces</ a > </ li >
71+ < li > < a href ="/agda_html/Leios.Voting.html " > Voting</ a > </ li >
72+ < li > < a href ="/agda_html/Leios.VRF.html " > VRF</ a > </ li >
73+ </ ul >
74+
75+ </ nav >
76+ < main class ="agda-content ">
77+ < script src ="agda.js "> </ script > < pre class ="Agda "> < div class ="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-universe-polymorphism</ a > </ div >
78+ < div class ="line "> < a id ="80 " class ="Pragma "> --no-sized-types</ a > < a id ="97 " class ="Pragma "> --no-guardedness</ a > < a id ="114 " class ="Pragma "> --level-universe</ a > < a id ="131 " class ="Symbol "> #-}</ a > </ div >
79+ < div class ="line "> </ div >
80+ < div class ="line "> < a id ="136 " class ="Keyword "> module</ a > < a id ="143 " href ="/agda_html/Agda.Builtin.Bool.html " class ="Module "> Agda.Builtin.Bool</ a > < a id ="161 " class ="Keyword "> where</ a > </ div >
81+ < div class ="line "> </ div >
82+ < div class ="line "> < a id ="168 " class ="Keyword "> data</ a > < a id ="Bool "> </ a > < a id ="173 " href ="/agda_html/Agda.Builtin.Bool.html#173 " class ="Datatype "> Bool</ a > < a id ="178 " class ="Symbol "> :</ a > < a id ="180 " href ="/agda_html/Agda.Primitive.html#388 " class ="Primitive "> Set</ a > < a id ="184 " class ="Keyword "> where</ a > </ div >
83+ < div class ="line "> < a id ="Bool.false "> </ a > < a id ="192 " href ="/agda_html/Agda.Builtin.Bool.html#192 " class ="InductiveConstructor "> false</ a > < a id ="Bool.true "> </ a > < a id ="198 " href ="/agda_html/Agda.Builtin.Bool.html#198 " class ="InductiveConstructor "> true</ a > < a id ="203 " class ="Symbol "> :</ a > < a id ="205 " href ="/agda_html/Agda.Builtin.Bool.html#173 " class ="Datatype "> Bool</ a > </ div >
84+ < div class ="line "> </ div >
85+ < div class ="line "> < a id ="211 " class ="Symbol "> {-#</ a > < a id ="215 " class ="Keyword "> BUILTIN</ a > < a id ="223 " class ="Keyword "> BOOL</ a > < a id ="229 " href ="/agda_html/Agda.Builtin.Bool.html#173 " class ="Datatype "> Bool</ a > < a id ="235 " class ="Symbol "> #-}</ a > </ div >
86+ < div class ="line "> < a id ="239 " class ="Symbol "> {-#</ a > < a id ="243 " class ="Keyword "> BUILTIN</ a > < a id ="251 " class ="Keyword "> FALSE</ a > < a id ="257 " href ="/agda_html/Agda.Builtin.Bool.html#192 " class ="InductiveConstructor "> false</ a > < a id ="263 " class ="Symbol "> #-}</ a > </ div >
87+ < div class ="line "> < a id ="267 " class ="Symbol "> {-#</ a > < a id ="271 " class ="Keyword "> BUILTIN</ a > < a id ="279 " class ="Keyword "> TRUE</ a > < a id ="285 " href ="/agda_html/Agda.Builtin.Bool.html#198 " class ="InductiveConstructor "> true</ a > < a id ="291 " class ="Symbol "> #-}</ a > </ div >
88+ < div class ="line "> </ div >
89+ < div class ="line "> < a id ="296 " class ="Symbol "> {-#</ a > < a id ="300 " class ="Keyword "> COMPILE</ a > < a id ="308 " class ="Keyword "> JS</ a > < a id ="311 " href ="/agda_html/Agda.Builtin.Bool.html#173 " class ="Datatype "> Bool</ a > < a id ="317 " class ="Pragma "> =</ a > < a id ="319 " class ="Pragma "> function</ a > < a id ="328 " class ="Pragma "> (x,v)</ a > < a id ="334 " class ="Pragma "> {</ a > < a id ="336 " class ="Pragma "> return</ a > < a id ="343 " class ="Pragma "> ((x)?</ a > < a id ="349 " class ="Pragma "> v["true"]()</ a > < a id ="361 " class ="Pragma "> :</ a > < a id ="363 " class ="Pragma "> v["false"]());</ a > < a id ="378 " class ="Pragma "> }</ a > < a id ="380 " class ="Symbol "> #-}</ a > </ div >
90+ < div class ="line "> < a id ="384 " class ="Symbol "> {-#</ a > < a id ="388 " class ="Keyword "> COMPILE</ a > < a id ="396 " class ="Keyword "> JS</ a > < a id ="399 " href ="/agda_html/Agda.Builtin.Bool.html#192 " class ="InductiveConstructor "> false</ a > < a id ="405 " class ="Pragma "> =</ a > < a id ="407 " class ="Pragma "> false</ a > < a id ="413 " class ="Symbol "> #-}</ a > </ div >
91+ < div class ="line "> < a id ="417 " class ="Symbol "> {-#</ a > < a id ="421 " class ="Keyword "> COMPILE</ a > < a id ="429 " class ="Keyword "> JS</ a > < a id ="432 " href ="/agda_html/Agda.Builtin.Bool.html#198 " class ="InductiveConstructor "> true</ a > < a id ="438 " class ="Pragma "> =</ a > < a id ="440 " class ="Pragma "> true</ a > < a id ="446 " class ="Symbol "> #-}</ a > </ div >
92+ < div class ="line "> </ div > </ pre > </ main > </ div > </ body > </ html >
0 commit comments