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
BadArgumentsToPatternSynonym	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BadImplicits	Agda.TypeChecking.Implicit
BadMacroDef	Agda.Syntax.Concrete.Definitions
BadVisibility	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Bag
1 (Type/Class)	Agda.Utils.Bag
2 (Data Constructor)	Agda.Utils.Bag
bag	Agda.Utils.Bag
begin	Agda.Syntax.Parser.LexActions
Beginning	Agda.Syntax.Common
beginningOf	Agda.Syntax.Position
beginningOfFile	Agda.Syntax.Position
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
benchmarkOn	Agda.Utils.Benchmark
benchmarks	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
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
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.Syntax.Internal
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
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
bindsWithHidingToTel	Agda.TypeChecking.Substitute
bindsWithHidingToTel'	Agda.TypeChecking.Substitute
bindTCMT	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
bindToConcrete	Agda.Syntax.Translation.AbstractToConcrete
bindUntypedBuiltin	Agda.TypeChecking.Rules.Builtin
bindVariable	Agda.Syntax.Scope.Monad
BinOp	Agda.Compiler.JS.Syntax
binop	Agda.Compiler.JS.Parser
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
BlockedOnMeta	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
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
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
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
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
boundToEverySome	Agda.TypeChecking.Positivity.Occurrence
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
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
bstringC	Agda.TypeChecking.Serialise.Base
bstringD	Agda.TypeChecking.Serialise.Base
bstringE	Agda.TypeChecking.Serialise.Base
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
buildPrimCases	Agda.Compiler.UHC.FromAgda
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
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
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
builtinAgdaTCMNormalise	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMQuoteTerm	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMReturn	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMTypeError	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnify	Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnquoteTerm	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
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
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
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
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.UHC.FromAgda
2 (Data Constructor)	Agda.Compiler.UHC.FromAgda
builtinKit	Agda.Compiler.UHC.FromAgda
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
BuiltinNoDefPragma	Agda.Syntax.Abstract
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
builtinRewrite	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
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
builtinTrue	Agda.TypeChecking.Monad.Builtin
builtinUnit	Agda.TypeChecking.Monad.Builtin
builtinUnitCtor	Agda.Compiler.UHC.MagicTypes
builtinUnitUnit	Agda.TypeChecking.Monad.Builtin
BuiltinUnknown	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinVisible	Agda.TypeChecking.Monad.Builtin
builtinZero	Agda.TypeChecking.Monad.Builtin