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
1 (Type/Class)	Agda.Compiler.Backend
2 (Data Constructor)	Agda.Compiler.Backend
Backend'
1 (Type/Class)	Agda.Compiler.Backend
2 (Data Constructor)	Agda.Compiler.Backend
backendInteraction	Agda.Compiler.Backend
BackendName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
backendName	Agda.Compiler.Backend
backendUsage	Agda.Main
backendVersion	Agda.Compiler.Backend
backupPos	Agda.Syntax.Position
BadArgumentsToPatternSynonym	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BadImplicits	Agda.TypeChecking.Implicit
BadMacroDef	Agda.Syntax.Concrete.Definitions
BadVisibility	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Bag
1 (Type/Class)	Agda.Utils.Bag
2 (Data Constructor)	Agda.Utils.Bag
bag	Agda.Utils.Bag
BDecls	Agda.Utils.Haskell.Syntax
begin	Agda.Syntax.Parser.LexActions
Beginning	Agda.Syntax.Common
beginningOf	Agda.Syntax.Position
beginningOfFile	Agda.Syntax.Position
beginWith	Agda.Syntax.Parser.LexActions
begin_	Agda.Syntax.Parser.LexActions
Benchmark
1 (Type/Class)	Agda.Utils.Benchmark
2 (Data Constructor)	Agda.Utils.Benchmark
3 (Type/Class)	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
BenchmarkOff	Agda.Utils.Benchmark
BenchmarkOn
1 (Type/Class)	Agda.Utils.Benchmark
2 (Data Constructor)	Agda.Utils.Benchmark
benchmarkOn	Agda.Utils.Benchmark
benchmarks	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
BenchmarkSome	Agda.Utils.Benchmark
bestConInfo	Agda.Syntax.Common
betareduce	Agda.Auto.CaseSplit
between	Agda.Utils.Parser.ReadP
Big
1 (Type/Class)	Agda.Syntax.Common
2 (Data Constructor)	Agda.Syntax.Common
billPureTo	Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billTo	Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billToCPS	Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billToIO	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
billToPure	Agda.Benchmarking, 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
BinaryEncode	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
bind	Agda.TypeChecking.Free.Lazy
bind'	Agda.TypeChecking.Free.Lazy
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
bindBuiltinNoDef	Agda.TypeChecking.Rules.Builtin
bindBuiltinSharp	Agda.TypeChecking.Rules.Builtin.Coinduction
Binder
1 (Type/Class)	Agda.Compiler.Treeless.Subst
2 (Data Constructor)	Agda.Compiler.Treeless.Subst
BindHole	Agda.Syntax.Notation
bindLHSVars	Agda.TypeChecking.Rules.LHS
bindModule	Agda.Syntax.Scope.Monad
bindName	Agda.Syntax.Scope.Monad
bindP	Agda.Utils.Parser.MemoisedCPS
bindParameters	Agda.TypeChecking.Rules.Data
bindParameters'	Agda.TypeChecking.Rules.Data
bindPostulatedName	Agda.TypeChecking.Rules.Builtin
bindPrimitive	Agda.TypeChecking.Monad.Builtin
bindQModule	Agda.Syntax.Scope.Monad
bindReduce	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Binds	Agda.Utils.Haskell.Syntax
bindsToTel	Agda.TypeChecking.Substitute
bindsToTel'	Agda.TypeChecking.Substitute
bindsWithHidingToTel	Agda.TypeChecking.Substitute
bindsWithHidingToTel'	Agda.TypeChecking.Substitute
bindTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
bindToConcrete	Agda.Syntax.Translation.AbstractToConcrete
bindUntypedBuiltin	Agda.TypeChecking.Rules.Builtin
bindVariable	Agda.Syntax.Scope.Monad
BinOp	Agda.Compiler.JS.Syntax
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, Agda.Compiler.Backend
BlockedLevel	Agda.Syntax.Internal
BlockedOnMeta	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Blocked_	Agda.Syntax.Internal
blockingMeta	Agda.Syntax.Internal
blockingStatus	Agda.Syntax.Internal
BlockingVar
1 (Type/Class)	Agda.TypeChecking.Coverage.Match
2 (Data Constructor)	Agda.TypeChecking.Coverage.Match
blockingVarCons	Agda.TypeChecking.Coverage.Match
blockingVarNo	Agda.TypeChecking.Coverage.Match
BlockingVars	Agda.TypeChecking.Coverage.Match
blockOfLines	Agda.Syntax.Scope.Base
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
bol	Agda.Syntax.Parser.Lexer
boolSemiring	Agda.Termination.Semiring
boolToMaybe	Agda.Utils.Maybe
bothAbsurd	Agda.TypeChecking.Conversion
BothWithAndRHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
botVarOcc	Agda.TypeChecking.Free.Lazy
Bound
1 (Type/Class)	Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)	Agda.Interaction.Highlighting.Precise
BoundedLt	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BoundedNo	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BoundedSize	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
boundToEverySome	Agda.TypeChecking.Positivity.Occurrence
br	Agda.Compiler.JS.Pretty
braces
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
braces'	Agda.Syntax.Concrete.Pretty
bracesAndSemicolons	Agda.Syntax.Concrete.Pretty
brackets
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
bracket_	Agda.Utils.Monad
Branches	Agda.TypeChecking.CompiledClause
bstringC	Agda.TypeChecking.Serialise.Base
bstringD	Agda.TypeChecking.Serialise.Base
bstringE	Agda.TypeChecking.Serialise.Base
buildClosure	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
buildConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
buildGraph	Agda.Utils.Warshall
BuildInterface	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
buildInterface	Agda.Interaction.Imports
buildList	Agda.TypeChecking.Primitive
buildOccurrenceGraph	Agda.TypeChecking.Positivity
buildPattern	Agda.TypeChecking.Coverage.Match
buildProblemConstraint	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
buildProblemConstraint_	Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
buildSubstitution	Agda.TypeChecking.Patterns.Match
buildWithFunction	Agda.TypeChecking.With
Builtin
1 (Type/Class)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinAbs	Agda.TypeChecking.Monad.Builtin
builtinAbsAbs	Agda.TypeChecking.Monad.Builtin
builtinAgdaClause	Agda.TypeChecking.Monad.Builtin
builtinAgdaClauseAbsurd	Agda.TypeChecking.Monad.Builtin
builtinAgdaClauseClause	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
builtinAgdaErrorPart	Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartName	Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartString	Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitChar	Agda.TypeChecking.Monad.Builtin
builtinAgdaLiteral	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitFloat	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitMeta	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitNat	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitQName	Agda.TypeChecking.Monad.Builtin
builtinAgdaLitString	Agda.TypeChecking.Monad.Builtin
builtinAgdaMeta	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatAbsurd	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatCon	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatDot	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatLit	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatProj	Agda.TypeChecking.Monad.Builtin
builtinAgdaPattern	Agda.TypeChecking.Monad.Builtin
builtinAgdaPatVar	Agda.TypeChecking.Monad.Builtin
builtinAgdaSort	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortLit	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortSet	Agda.TypeChecking.Monad.Builtin
builtinAgdaSortUnsupported	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCM	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMBind	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMBlockOnMeta	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCatchError	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCheckType	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCommit	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDebugPrint	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDeclareDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDefineFun	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMExtendContext	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMFreshName	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetContext	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetDefinition	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetType	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMInContext	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMInferType	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMIsMacro	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMNormalise	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMQuoteTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMReduce	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMReturn	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMTypeError	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnify	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnquoteTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMWithNormalisation	Agda.TypeChecking.Monad.Builtin
builtinAgdaTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermCon	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermDef	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermExtLam	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermLam	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermLit	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermMeta	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermPi	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermSort	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermUnsupported	Agda.TypeChecking.Monad.Builtin
builtinAgdaTermVar	Agda.TypeChecking.Monad.Builtin
builtinArg	Agda.TypeChecking.Monad.Builtin
builtinArgArg	Agda.TypeChecking.Monad.Builtin
builtinArgArgInfo	Agda.TypeChecking.Monad.Builtin
builtinArgInfo	Agda.TypeChecking.Monad.Builtin
builtinAssoc	Agda.TypeChecking.Monad.Builtin
builtinAssocLeft	Agda.TypeChecking.Monad.Builtin
builtinAssocNon	Agda.TypeChecking.Monad.Builtin
builtinAssocRight	Agda.TypeChecking.Monad.Builtin
builtinBackends	Agda.Main
builtinBool	Agda.TypeChecking.Monad.Builtin
builtinChar	Agda.TypeChecking.Monad.Builtin
builtinCons	Agda.TypeChecking.Monad.Builtin
BuiltinData	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BuiltinDataCons	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinDesc	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BuiltinDescriptor	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinEquality	Agda.TypeChecking.Monad.Builtin
builtinFalse	Agda.TypeChecking.Monad.Builtin
builtinFixity	Agda.TypeChecking.Monad.Builtin
builtinFixityFixity	Agda.TypeChecking.Monad.Builtin
builtinFlat	Agda.TypeChecking.Monad.Builtin
builtinFloat	Agda.TypeChecking.Monad.Builtin
builtinFromNat	Agda.TypeChecking.Monad.Builtin
builtinFromNeg	Agda.TypeChecking.Monad.Builtin
builtinFromString	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, Agda.Compiler.Backend
2 (Data Constructor)	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BuiltinInParameterisedModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinInstance	Agda.TypeChecking.Monad.Builtin
builtinInteger	Agda.TypeChecking.Monad.Builtin
builtinIntegerNegSuc	Agda.TypeChecking.Monad.Builtin
builtinIntegerPos	Agda.TypeChecking.Monad.Builtin
builtinIO	Agda.TypeChecking.Monad.Builtin
builtinIrrelevant	Agda.TypeChecking.Monad.Builtin
BuiltinKit
1 (Type/Class)	Agda.Compiler.Treeless.EliminateLiteralPatterns
2 (Data Constructor)	Agda.Compiler.Treeless.EliminateLiteralPatterns
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, Agda.Compiler.Backend
builtinName	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
BuiltinNoDefPragma	Agda.Syntax.Abstract
BuiltinPostulate	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
BuiltinPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
builtinPrecedence	Agda.TypeChecking.Monad.Builtin
builtinPrecRelated	Agda.TypeChecking.Monad.Builtin
builtinPrecUnrelated	Agda.TypeChecking.Monad.Builtin
BuiltinPrim	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinQName	Agda.TypeChecking.Monad.Builtin
builtinRefl	Agda.TypeChecking.Monad.Builtin
builtinRelevance	Agda.TypeChecking.Monad.Builtin
builtinRelevant	Agda.TypeChecking.Monad.Builtin
builtinRewrite	Agda.TypeChecking.Monad.Builtin
builtinSharp	Agda.TypeChecking.Monad.Builtin
builtinSize	Agda.TypeChecking.Monad.Builtin
builtinSizeHook	Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinSizeInf	Agda.TypeChecking.Monad.Builtin
builtinSizeLt	Agda.TypeChecking.Monad.Builtin
builtinSizeMax	Agda.TypeChecking.Monad.Builtin
builtinSizeSuc	Agda.TypeChecking.Monad.Builtin
builtinSizeUniv	Agda.TypeChecking.Monad.Builtin
builtinsNoDef	Agda.TypeChecking.Monad.Builtin
builtinString	Agda.TypeChecking.Monad.Builtin
builtinSuc	Agda.TypeChecking.Monad.Builtin
BuiltinThings	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinTrue	Agda.TypeChecking.Monad.Builtin
builtinUnit	Agda.TypeChecking.Monad.Builtin
builtinUnitUnit	Agda.TypeChecking.Monad.Builtin
BuiltinUnknown	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
builtinVisible	Agda.TypeChecking.Monad.Builtin
builtinZero	Agda.TypeChecking.Monad.Builtin