Sophie

Sophie

distrib > Fedora > 19 > i386 > by-pkgid > 6141746cd5048a6ddf1cf3194274ce61 > files > 947

ghc-Agda-devel-2.3.2.1-5.fc19.i686.rpm

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda-2.3.2.1: A dependently typed functional programming language and proof assistant (Index - B)</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="alphabet"><ul><li><a href="doc-index-A.html">A</a></li><li><a href="doc-index-B.html">B</a></li><li><a href="doc-index-C.html">C</a></li><li><a href="doc-index-D.html">D</a></li><li><a href="doc-index-E.html">E</a></li><li><a href="doc-index-F.html">F</a></li><li><a href="doc-index-G.html">G</a></li><li><a href="doc-index-H.html">H</a></li><li><a href="doc-index-I.html">I</a></li><li><a href="doc-index-J.html">J</a></li><li><a href="doc-index-K.html">K</a></li><li><a href="doc-index-L.html">L</a></li><li><a href="doc-index-M.html">M</a></li><li><a href="doc-index-N.html">N</a></li><li><a href="doc-index-O.html">O</a></li><li><a href="doc-index-P.html">P</a></li><li><a href="doc-index-Q.html">Q</a></li><li><a href="doc-index-R.html">R</a></li><li><a href="doc-index-S.html">S</a></li><li><a href="doc-index-T.html">T</a></li><li><a href="doc-index-U.html">U</a></li><li><a href="doc-index-V.html">V</a></li><li><a href="doc-index-W.html">W</a></li><li><a href="doc-index-X.html">X</a></li><li><a href="doc-index-Y.html">Y</a></li><li><a href="doc-index-Z.html">Z</a></li><li><a href="doc-index-58.html">:</a></li><li><a href="doc-index-33.html">!</a></li><li><a href="doc-index-36.html">$</a></li><li><a href="doc-index-38.html">&amp;</a></li><li><a href="doc-index-43.html">+</a></li><li><a href="doc-index-46.html">.</a></li><li><a href="doc-index-47.html">/</a></li><li><a href="doc-index-60.html">&lt;</a></li><li><a href="doc-index-61.html">=</a></li><li><a href="doc-index-62.html">&gt;</a></li><li><a href="doc-index-124.html">|</a></li><li><a href="doc-index-45.html">-</a></li><li><a href="doc-index-All.html">All</a></li></ul></div><div id="index"><p class="caption">Index - B</p><table><tr><td class="src">B</td><td class="module"><a href="Agda-Utils-Map.html#v:B">Agda.Utils.Map</a></td></tr><tr><td class="src">Backend</td><td class="module"><a href="Agda-Interaction-InteractionTop.html#t:Backend">Agda.Interaction.InteractionTop</a></td></tr><tr><td class="src">backupPos</td><td class="module"><a href="Agda-Syntax-Position.html#v:backupPos">Agda.Syntax.Position</a></td></tr><tr><td class="src">BadImplicits</td><td class="module"><a href="Agda-TypeChecking-Implicit.html#v:BadImplicits">Agda.TypeChecking.Implicit</a></td></tr><tr><td class="src">begin</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:begin">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">beginningOf</td><td class="module"><a href="Agda-Syntax-Position.html#v:beginningOf">Agda.Syntax.Position</a></td></tr><tr><td class="src">beginningOfFile</td><td class="module"><a href="Agda-Syntax-Position.html#v:beginningOfFile">Agda.Syntax.Position</a></td></tr><tr><td class="src">begin_</td><td class="module"><a href="Agda-Syntax-Parser-LexActions.html#v:begin_">Agda.Syntax.Parser.LexActions</a></td></tr><tr><td class="src">betareduce</td><td class="module"><a href="Agda-Auto-CaseSplit.html#v:betareduce">Agda.Auto.CaseSplit</a></td></tr><tr><td class="src">between</td><td class="module"><a href="Agda-Utils-ReadP.html#v:between">Agda.Utils.ReadP</a></td></tr><tr><td class="src">BinAppView</td><td class="module"><a href="Agda-TypeChecking-EtaContract.html#t:BinAppView">Agda.TypeChecking.EtaContract</a></td></tr><tr><td class="src">binAppView</td><td class="module"><a href="Agda-TypeChecking-EtaContract.html#v:binAppView">Agda.TypeChecking.EtaContract</a></td></tr><tr><td class="src">Bind</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Bind">Agda.Syntax.Internal</a></td></tr><tr><td class="src">bindAsPatterns</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS.html#v:bindAsPatterns">Agda.TypeChecking.Rules.LHS</a></td></tr><tr><td class="src">bindBuiltin</td><td class="module"><a href="Agda-TypeChecking-Rules-Builtin.html#v:bindBuiltin">Agda.TypeChecking.Rules.Builtin</a></td></tr><tr><td class="src">bindBuiltinFlat</td><td class="module"><a href="Agda-TypeChecking-Rules-Builtin-Coinduction.html#v:bindBuiltinFlat">Agda.TypeChecking.Rules.Builtin.Coinduction</a></td></tr><tr><td class="src">bindBuiltinInf</td><td class="module"><a href="Agda-TypeChecking-Rules-Builtin-Coinduction.html#v:bindBuiltinInf">Agda.TypeChecking.Rules.Builtin.Coinduction</a></td></tr><tr><td class="src">bindBuiltinName</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:bindBuiltinName">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">bindBuiltinSharp</td><td class="module"><a href="Agda-TypeChecking-Rules-Builtin-Coinduction.html#v:bindBuiltinSharp">Agda.TypeChecking.Rules.Builtin.Coinduction</a></td></tr><tr><td class="src">bindExpr</td><td class="module"><a href="Agda-Compiler-Epic-CompileState.html#v:bindExpr">Agda.Compiler.Epic.CompileState</a></td></tr><tr><td class="src">BindHole</td><td class="module"><a href="Agda-Syntax-Notation.html#v:BindHole">Agda.Syntax.Notation</a></td></tr><tr><td class="src">bindLHSVars</td><td class="module"><a href="Agda-TypeChecking-Rules-LHS.html#v:bindLHSVars">Agda.TypeChecking.Rules.LHS</a></td></tr><tr><td class="src">bindModule</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:bindModule">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">bindName</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:bindName">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">bindParameters</td><td class="module"><a href="Agda-TypeChecking-Rules-Data.html#v:bindParameters">Agda.TypeChecking.Rules.Data</a></td></tr><tr><td class="src">bindPostulatedName</td><td class="module"><a href="Agda-TypeChecking-Rules-Builtin.html#v:bindPostulatedName">Agda.TypeChecking.Rules.Builtin</a></td></tr><tr><td class="src">bindPrimitive</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:bindPrimitive">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">bindQModule</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:bindQModule">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">bindTCMT</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:bindTCMT">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">bindToConcrete</td><td class="module"><a href="Agda-Syntax-Translation-AbstractToConcrete.html#v:bindToConcrete">Agda.Syntax.Translation.AbstractToConcrete</a></td></tr><tr><td class="src">bindVariable</td><td class="module"><a href="Agda-Syntax-Scope-Monad.html#v:bindVariable">Agda.Syntax.Scope.Monad</a></td></tr><tr><td class="src">BinOp</td><td class="module"><a href="Agda-Compiler-JS-Syntax.html#v:BinOp">Agda.Compiler.JS.Syntax</a></td></tr><tr><td class="src">binop</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:binop">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Syntax-Concrete-Operators-Parser.html#v:binop">Agda.Syntax.Concrete.Operators.Parser</a></td></tr><tr><td class="src">blendInAbsurdClause</td><td class="module"><a href="Agda-TypeChecking-Coverage.html#v:blendInAbsurdClause">Agda.TypeChecking.Coverage</a></td></tr><tr><td class="src">Blind</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module">Agda.Utils.QuickCheck</td></tr><tr><td class="src">BlkInfo</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#t:BlkInfo">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="src">Block</td><td class="module"><a href="Agda-TypeChecking-Coverage-Match.html#v:Block">Agda.TypeChecking.Coverage.Match</a></td></tr><tr><td class="src">block</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:block">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">block'</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:block-39-">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">Blocked</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Auto-NarrowingSearch.html#v:Blocked">Agda.Auto.NarrowingSearch</a></td></tr><tr><td class="alt">2 (Type/Class)</td><td class="module"><a href="Agda-Syntax-Internal.html#t:Blocked">Agda.Syntax.Internal</a></td></tr><tr><td class="alt">3 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Blocked">Agda.Syntax.Internal</a></td></tr><tr><td class="src">blocked</td><td class="module"><a href="Agda-Syntax-Internal.html#v:blocked">Agda.Syntax.Internal</a></td></tr><tr><td class="src">BlockedConst</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BlockedConst">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BlockedLevel</td><td class="module"><a href="Agda-Syntax-Internal.html#v:BlockedLevel">Agda.Syntax.Internal</a></td></tr><tr><td class="src">blockingMeta</td><td class="module"><a href="Agda-Syntax-Internal.html#v:blockingMeta">Agda.Syntax.Internal</a></td></tr><tr><td class="src">BlockingVar</td><td class="module"><a href="Agda-TypeChecking-Coverage-Match.html#t:BlockingVar">Agda.TypeChecking.Coverage.Match</a></td></tr><tr><td class="src">BlockingVars</td><td class="module"><a href="Agda-TypeChecking-Coverage-Match.html#t:BlockingVars">Agda.TypeChecking.Coverage.Match</a></td></tr><tr><td class="src">blockOfLines</td><td class="module"><a href="Agda-Syntax-Scope-Base.html#v:blockOfLines">Agda.Syntax.Scope.Base</a></td></tr><tr><td class="src">blockTerm</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:blockTerm">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">blockTermOnProblem</td><td class="module"><a href="Agda-TypeChecking-MetaVars.html#v:blockTermOnProblem">Agda.TypeChecking.MetaVars</a></td></tr><tr><td class="src">bltQual</td><td class="module"><a href="Agda-Compiler-MAlonzo-Misc.html#v:bltQual">Agda.Compiler.MAlonzo.Misc</a></td></tr><tr><td class="src">bltQual'</td><td class="module"><a href="Agda-Compiler-MAlonzo-Primitives.html#v:bltQual-39-">Agda.Compiler.MAlonzo.Primitives</a></td></tr><tr><td class="src">BName</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:BName">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">bnameFixity</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:bnameFixity">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">Body</td><td class="module"><a href="Agda-Syntax-Internal.html#v:Body">Agda.Syntax.Internal</a></td></tr><tr><td class="src">body</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Case.html#v:body">Agda.Compiler.JS.Case</a></td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-Compiler-JS-Compiler.html#v:body">Agda.Compiler.JS.Compiler</a></td></tr><tr><td class="src">bol</td><td class="module"><a href="Agda-Syntax-Parser-Lexer.html#v:bol">Agda.Syntax.Parser.Lexer</a></td></tr><tr><td class="src">boolPrimTF</td><td class="module"><a href="Agda-Compiler-Epic-Primitive.html#v:boolPrimTF">Agda.Compiler.Epic.Primitive</a></td></tr><tr><td class="src">boolSemiring</td><td class="module"><a href="Agda-Termination-Semiring.html#v:boolSemiring">Agda.Termination.Semiring</a></td></tr><tr><td class="src">BothWithAndRHS</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BothWithAndRHS">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">Bound</td><td class="module"><a href="Agda-Interaction-Highlighting-Precise.html#v:Bound">Agda.Interaction.Highlighting.Precise</a></td></tr><tr><td class="src">BoundedLt</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#v:BoundedLt">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BoundedNo</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#v:BoundedNo">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BoundedSize</td><td class="module"><a href="Agda-TypeChecking-Monad-SizedTypes.html#t:BoundedSize">Agda.TypeChecking.Monad.SizedTypes</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">boundedSizeMetaHook</td><td class="module"><a href="Agda-TypeChecking-SizedTypes.html#v:boundedSizeMetaHook">Agda.TypeChecking.SizedTypes</a></td></tr><tr><td class="src">BoundName</td><td class="module"><a href="Agda-Syntax-Concrete.html#t:BoundName">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">boundName</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:boundName">Agda.Syntax.Concrete</a></td></tr><tr><td class="src">br</td><td class="module"><a href="Agda-Compiler-JS-Pretty.html#v:br">Agda.Compiler.JS.Pretty</a></td></tr><tr><td class="src">braced</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:braced">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">bracedBlock</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:bracedBlock">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">braces</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:braces">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">braces'</td><td class="module"><a href="Agda-Syntax-Concrete-Pretty.html#v:braces-39-">Agda.Syntax.Concrete.Pretty</a></td></tr><tr><td class="src">bracket</td><td class="module"><a href="Agda-Utils-Monad.html#v:bracket">Agda.Utils.Monad</a></td></tr><tr><td class="src">bracketed</td><td class="module"><a href="Agda-Compiler-JS-Parser.html#v:bracketed">Agda.Compiler.JS.Parser</a></td></tr><tr><td class="src">brackets</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Function)</td><td class="module">Agda.Utils.Pretty</td></tr><tr><td class="alt">2 (Function)</td><td class="module"><a href="Agda-TypeChecking-Pretty.html#v:brackets">Agda.TypeChecking.Pretty</a></td></tr><tr><td class="src">bracket_</td><td class="module"><a href="Agda-Utils-Monad.html#v:bracket_">Agda.Utils.Monad</a></td></tr><tr><td class="src">Branch</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#t:Branch">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:Branch">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">Branches</td><td class="module"><a href="Agda-TypeChecking-CompiledClause.html#v:Branches">Agda.TypeChecking.CompiledClause</a></td></tr><tr><td class="src">brExpr</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:brExpr">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">BrInt</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:BrInt">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">brInt</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:brInt">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">brName</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:brName">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">brTag</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:brTag">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">brVars</td><td class="module"><a href="Agda-Compiler-Epic-AuxAST.html#v:brVars">Agda.Compiler.Epic.AuxAST</a></td></tr><tr><td class="src">buildClosure</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:buildClosure">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">buildConstraint</td><td class="module"><a href="Agda-TypeChecking-Monad-Constraints.html#v:buildConstraint">Agda.TypeChecking.Monad.Constraints</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">buildGraph</td><td class="module"><a href="Agda-Utils-Warshall.html#v:buildGraph">Agda.Utils.Warshall</a></td></tr><tr><td class="src">buildInterface</td><td class="module"><a href="Agda-Interaction-Imports.html#v:buildInterface">Agda.Interaction.Imports</a></td></tr><tr><td class="src">buildLambda</td><td class="module"><a href="Agda-Compiler-Epic-Smashing.html#v:buildLambda">Agda.Compiler.Epic.Smashing</a></td></tr><tr><td class="src">buildList</td><td class="module"><a href="Agda-TypeChecking-Primitive.html#v:buildList">Agda.TypeChecking.Primitive</a></td></tr><tr><td class="src">buildMPatterns</td><td class="module"><a href="Agda-TypeChecking-Coverage-Match.html#v:buildMPatterns">Agda.TypeChecking.Coverage.Match</a></td></tr><tr><td class="src">buildOccurrenceGraph</td><td class="module"><a href="Agda-TypeChecking-Positivity.html#v:buildOccurrenceGraph">Agda.TypeChecking.Positivity</a></td></tr><tr><td class="src">buildParser</td><td class="module"><a href="Agda-Syntax-Concrete-Operators.html#v:buildParser">Agda.Syntax.Concrete.Operators</a></td></tr><tr><td class="src">buildProblemConstraint</td><td class="module"><a href="Agda-TypeChecking-Monad-Constraints.html#v:buildProblemConstraint">Agda.TypeChecking.Monad.Constraints</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">buildTerm</td><td class="module"><a href="Agda-Compiler-Epic-Forcing.html#v:buildTerm">Agda.Compiler.Epic.Forcing</a></td></tr><tr><td class="src">buildWithFunction</td><td class="module"><a href="Agda-TypeChecking-With.html#v:buildWithFunction">Agda.TypeChecking.With</a></td></tr><tr><td class="src">Builtin</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:Builtin">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:Builtin">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinAgdaDataDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDataDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinition</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinition">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionDataConstructor</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionDataConstructor">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionDataDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionDataDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionFunDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionFunDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionPostulate</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionPostulate">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionPrimitive</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionPrimitive">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaDefinitionRecordDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaDefinitionRecordDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaFunDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaFunDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaRecordDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaRecordDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaSort</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaSort">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaSortLit</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaSortLit">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaSortSet</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaSortSet">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaSortUnsupported</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaSortUnsupported">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTerm</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTerm">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermCon</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermCon">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermDef</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermDef">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermLam</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermLam">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermPi</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermPi">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermSort</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermSort">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermUnsupported</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermUnsupported">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTermVar</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTermVar">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaType</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaType">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinAgdaTypeEl</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinAgdaTypeEl">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinArg</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinArg">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinArgArg</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinArgArg">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinBool</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinBool">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinChar</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinChar">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinCons</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinCons">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinData</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinData">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BuiltinDataCons</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinDataCons">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinDesc</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:builtinDesc">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BuiltinDescriptor</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:BuiltinDescriptor">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinEquality</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinEquality">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinFalse</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinFalse">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinFlat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinFlat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinFloat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinFloat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinHidden</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinHidden">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinHiding</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinHiding">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinInf</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinInf">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinInfo</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Type/Class)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:BuiltinInfo">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinInfo">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BuiltinInParameterisedModule</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinInParameterisedModule">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinInstance</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinInstance">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinInteger</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinInteger">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinIO</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinIO">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinIrrAxiom</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinIrrAxiom">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinIrrelevant</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinIrrelevant">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinLevel</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinLevel">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinLevelKit</td><td class="module"><a href="Agda-TypeChecking-Level.html#v:builtinLevelKit">Agda.TypeChecking.Level</a></td></tr><tr><td class="src">builtinLevelMax</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinLevelMax">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinLevelSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinLevelSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinLevelZero</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinLevelZero">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinList</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinList">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinMustBeConstructor</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinMustBeConstructor">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinName</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:builtinName">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinNat</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNat">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatDivSucAux</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatDivSucAux">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatEquals</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatEquals">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatLess</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatLess">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatMinus</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatMinus">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatModSucAux</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatModSucAux">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatPlus</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatPlus">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNatTimes</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNatTimes">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinNil</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinNil">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinPostulate</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinPostulate">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">BuiltinPragma</td><td>&nbsp;</td></tr><tr><td class="alt">1 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Concrete.html#v:BuiltinPragma">Agda.Syntax.Concrete</a></td></tr><tr><td class="alt">2 (Data Constructor)</td><td class="module"><a href="Agda-Syntax-Abstract.html#v:BuiltinPragma">Agda.Syntax.Abstract</a></td></tr><tr><td class="src">BuiltinPrim</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinPrim">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinQName</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinQName">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinRefl</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinRefl">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinRelevance</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinRelevance">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinRelevant</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinRelevant">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSharp</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSharp">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSize</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSize">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSizeHook</td><td class="module"><a href="Agda-TypeChecking-SizedTypes.html#v:builtinSizeHook">Agda.TypeChecking.SizedTypes</a></td></tr><tr><td class="src">builtinSizeInf</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSizeInf">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSizeLt</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSizeLt">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSizeMax</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSizeMax">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSizeSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSizeSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinString</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinString">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinSuc</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinSuc">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinThings</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#t:BuiltinThings">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinTrue</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinTrue">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">BuiltinUnknown</td><td class="module"><a href="Agda-TypeChecking-Monad-Base.html#v:BuiltinUnknown">Agda.TypeChecking.Monad.Base</a>, Agda.TypeChecking.Monad</td></tr><tr><td class="src">builtinVisible</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinVisible">Agda.TypeChecking.Monad.Builtin</a></td></tr><tr><td class="src">builtinZero</td><td class="module"><a href="Agda-TypeChecking-Monad-Builtin.html#v:builtinZero">Agda.TypeChecking.Monad.Builtin</a></td></tr></table></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>