A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
$
&
+
.
/
<
=
>
|
-
All

Index - B

B	Agda.Utils.Map
Backend	Agda.Interaction.InteractionTop
backupPos	Agda.Syntax.Position
BadImplicits	Agda.TypeChecking.Implicit
begin	Agda.Syntax.Parser.LexActions
beginningOf	Agda.Syntax.Position
beginningOfFile	Agda.Syntax.Position
begin_	Agda.Syntax.Parser.LexActions
Benchmark	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
benchmarking	Agda.TypeChecking.Monad.Benchmark
betareduce	Agda.Auto.CaseSplit
between	Agda.Utils.ReadP
billPureTo	Agda.TypeChecking.Monad.Benchmark
billSub	Agda.TypeChecking.Monad.Benchmark
billTo	Agda.TypeChecking.Monad.Benchmark
billTop	Agda.TypeChecking.Monad.Benchmark
BiMap
1 (Type/Class)	Agda.Utils.BiMap
2 (Data Constructor)	Agda.Utils.BiMap
biMapBack	Agda.Utils.BiMap
biMapThere	Agda.Utils.BiMap
BinAppView	Agda.TypeChecking.EtaContract
binAppView	Agda.TypeChecking.EtaContract
Bind	Agda.Syntax.Internal
bindAsPatterns	Agda.TypeChecking.Rules.LHS
bindBuiltin	Agda.TypeChecking.Rules.Builtin
bindBuiltinFlat	Agda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInf	Agda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinName	Agda.TypeChecking.Monad.Builtin
bindBuiltinSharp	Agda.TypeChecking.Rules.Builtin.Coinduction
bindExpr	Agda.Compiler.Epic.CompileState
BindHole	Agda.Syntax.Notation
bindLHSVars	Agda.TypeChecking.Rules.LHS
bindModule	Agda.Syntax.Scope.Monad
bindName	Agda.Syntax.Scope.Monad
bindParameters	Agda.TypeChecking.Rules.Data
bindPostulatedName	Agda.TypeChecking.Rules.Builtin
bindPrimitive	Agda.TypeChecking.Monad.Builtin
bindQModule	Agda.Syntax.Scope.Monad
bindsToTel	Agda.TypeChecking.Substitute
bindsToTel'	Agda.TypeChecking.Substitute
bindTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
bindToConcrete	Agda.Syntax.Translation.AbstractToConcrete
bindVariable	Agda.Syntax.Scope.Monad
BinOp	Agda.Compiler.JS.Syntax
binop
1 (Function)	Agda.Compiler.JS.Parser
2 (Function)	Agda.Syntax.Concrete.Operators.Parser
blendInAbsurdClause	Agda.TypeChecking.Coverage
Blind
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
BlkInfo	Agda.Auto.NarrowingSearch
Block	Agda.TypeChecking.Coverage.Match
block	Agda.Compiler.JS.Pretty
block'	Agda.Compiler.JS.Pretty
Blocked
1 (Data Constructor)	Agda.Auto.NarrowingSearch
2 (Type/Class)	Agda.Syntax.Internal
3 (Data Constructor)	Agda.Syntax.Internal
blocked	Agda.Syntax.Internal
BlockedConst	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BlockedLevel	Agda.Syntax.Internal
blockingMeta	Agda.Syntax.Internal
BlockingVar	Agda.TypeChecking.Coverage.Match
BlockingVars	Agda.TypeChecking.Coverage.Match
blockOfLines	Agda.Syntax.Scope.Base
BlockP	Agda.TypeChecking.Coverage.Match
blockTerm	Agda.TypeChecking.MetaVars
blockTermOnProblem	Agda.TypeChecking.MetaVars
blockTypeOnProblem	Agda.TypeChecking.MetaVars
bltQual	Agda.Compiler.MAlonzo.Misc
bltQual'	Agda.Compiler.MAlonzo.Primitives
BName	Agda.Syntax.Concrete
bnameFixity	Agda.Syntax.Concrete
Body	Agda.Syntax.Internal
body
1 (Function)	Agda.Compiler.JS.Case
2 (Function)	Agda.Compiler.JS.Compiler
bol	Agda.Syntax.Parser.Lexer
boolPrimTF	Agda.Compiler.Epic.Primitive
boolSemiring	Agda.Termination.Semiring
bothAbsurd	Agda.TypeChecking.Conversion
BothWithAndRHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Bound
1 (Type/Class)	Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
BoundedLt	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
BoundedNo	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
BoundedSize	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
boundedSizeMetaHook	Agda.TypeChecking.SizedTypes
boundLabel	Agda.Syntax.Concrete
BoundName	Agda.Syntax.Concrete
boundName	Agda.Syntax.Concrete
Bounds
1 (Type/Class)	Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)	Agda.TypeChecking.SizedTypes.WarshallSolver
bounds	Agda.TypeChecking.SizedTypes.WarshallSolver
br	Agda.Compiler.JS.Pretty
braced	Agda.Compiler.JS.Parser
bracedBlock	Agda.Compiler.JS.Parser
braces
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
braces'	Agda.Syntax.Concrete.Pretty
bracesAndSemicolons	Agda.Syntax.Concrete.Pretty
bracket	Agda.Utils.Monad
bracketed	Agda.Compiler.JS.Parser
brackets
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
bracket_	Agda.Utils.Monad
Branch
1 (Type/Class)	Agda.Compiler.Epic.AuxAST
2 (Data Constructor)	Agda.Compiler.Epic.AuxAST
Branches	Agda.TypeChecking.CompiledClause
brExpr	Agda.Compiler.Epic.AuxAST
BrInt	Agda.Compiler.Epic.AuxAST
brInt	Agda.Compiler.Epic.AuxAST
brName	Agda.Compiler.Epic.AuxAST
brTag	Agda.Compiler.Epic.AuxAST
brVars	Agda.Compiler.Epic.AuxAST
buildClosure	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
buildConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildGraph	Agda.Utils.Warshall
buildInterface	Agda.Interaction.Imports
buildLambda	Agda.Compiler.Epic.Smashing
buildList	Agda.TypeChecking.Primitive
buildMPatterns	Agda.TypeChecking.Coverage.Match
buildOccurrenceGraph	Agda.TypeChecking.Positivity
BuildParser	Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
buildParser	Agda.Syntax.Concrete.Operators
buildProblemConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildTerm	Agda.Compiler.Epic.Forcing
buildWithFunction	Agda.TypeChecking.With
Builtin
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinAgdaDataDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinition	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataConstructor	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionFunDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPostulate	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPrimitive	Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionRecordDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaFunDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaRecordDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaSort	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortLit	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortSet	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortUnsupported	Agda.TypeChecking.Monad.Builtin
builtinAgdaTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermCon	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermLam	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermPi	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermSort	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermUnsupported	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermVar	Agda.TypeChecking.Monad.Builtin
builtinAgdaType	Agda.TypeChecking.Monad.Builtin
builtinAgdaTypeEl	Agda.TypeChecking.Monad.Builtin
builtinArg	Agda.TypeChecking.Monad.Builtin
builtinArgArg	Agda.TypeChecking.Monad.Builtin
builtinArgArgInfo	Agda.TypeChecking.Monad.Builtin
builtinArgInfo	Agda.TypeChecking.Monad.Builtin
builtinBool	Agda.TypeChecking.Monad.Builtin
builtinChar	Agda.TypeChecking.Monad.Builtin
builtinCons	Agda.TypeChecking.Monad.Builtin
BuiltinData	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDataCons	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinDesc	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDescriptor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinEquality	Agda.TypeChecking.Monad.Builtin
builtinFalse	Agda.TypeChecking.Monad.Builtin
builtinFlat	Agda.TypeChecking.Monad.Builtin
builtinFloat	Agda.TypeChecking.Monad.Builtin
builtinHidden	Agda.TypeChecking.Monad.Builtin
builtinHiding	Agda.TypeChecking.Monad.Builtin
builtinInf	Agda.TypeChecking.Monad.Builtin
BuiltinInfo
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinInParameterisedModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinInstance	Agda.TypeChecking.Monad.Builtin
builtinInteger	Agda.TypeChecking.Monad.Builtin
builtinIO	Agda.TypeChecking.Monad.Builtin
builtinIrrAxiom	Agda.TypeChecking.Monad.Builtin
builtinIrrelevant	Agda.TypeChecking.Monad.Builtin
builtinLevel	Agda.TypeChecking.Monad.Builtin
builtinLevelKit	Agda.TypeChecking.Level
builtinLevelMax	Agda.TypeChecking.Monad.Builtin
builtinLevelSuc	Agda.TypeChecking.Monad.Builtin
builtinLevelZero	Agda.TypeChecking.Monad.Builtin
builtinList	Agda.TypeChecking.Monad.Builtin
BuiltinMustBeConstructor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinNat	Agda.TypeChecking.Monad.Builtin
builtinNatDivSucAux	Agda.TypeChecking.Monad.Builtin
builtinNatEquals	Agda.TypeChecking.Monad.Builtin
builtinNatLess	Agda.TypeChecking.Monad.Builtin
builtinNatMinus	Agda.TypeChecking.Monad.Builtin
builtinNatModSucAux	Agda.TypeChecking.Monad.Builtin
builtinNatPlus	Agda.TypeChecking.Monad.Builtin
builtinNatTimes	Agda.TypeChecking.Monad.Builtin
builtinNil	Agda.TypeChecking.Monad.Builtin
BuiltinPostulate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
BuiltinPrim	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinQName	Agda.TypeChecking.Monad.Builtin
builtinRefl	Agda.TypeChecking.Monad.Builtin
builtinRelevance	Agda.TypeChecking.Monad.Builtin
builtinRelevant	Agda.TypeChecking.Monad.Builtin
builtinSharp	Agda.TypeChecking.Monad.Builtin
builtinSize	Agda.TypeChecking.Monad.Builtin
builtinSizeHook	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
builtinSizeInf	Agda.TypeChecking.Monad.Builtin
builtinSizeLt	Agda.TypeChecking.Monad.Builtin
builtinSizeMax	Agda.TypeChecking.Monad.Builtin
builtinSizeSuc	Agda.TypeChecking.Monad.Builtin
builtinString	Agda.TypeChecking.Monad.Builtin
builtinSuc	Agda.TypeChecking.Monad.Builtin
BuiltinThings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinTrue	Agda.TypeChecking.Monad.Builtin
BuiltinUnknown	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinVisible	Agda.TypeChecking.Monad.Builtin
builtinZero	Agda.TypeChecking.Monad.Builtin