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.GhciTop
backupPos	Agda.Syntax.Position, Agda.Interaction.GhciTop
BadImplicits	Agda.TypeChecking.Implicit
begin	Agda.Syntax.Parser.LexActions
beginningOf	Agda.Syntax.Position, Agda.Interaction.GhciTop
beginningOfFile	Agda.Syntax.Position, Agda.Interaction.GhciTop
begin_	Agda.Syntax.Parser.LexActions
betareduce	Agda.Auto.CaseSplit
between	Agda.Utils.ReadP
BinAppView	Agda.TypeChecking.EtaContract
binAppView	Agda.TypeChecking.EtaContract
Bind	Agda.Syntax.Internal
bindAsPatterns	Agda.TypeChecking.Rules.LHS
bindBuiltin	Agda.TypeChecking.Rules.Builtin
bindBuiltinBool	Agda.TypeChecking.Rules.Builtin
bindBuiltinCons	Agda.TypeChecking.Rules.Builtin
bindBuiltinDummyConstructor	Agda.TypeChecking.Rules.Builtin
bindBuiltinEquality	Agda.TypeChecking.Rules.Builtin
bindBuiltinFlat	Agda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInf	Agda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinLevelSuc	Agda.TypeChecking.Rules.Builtin
bindBuiltinLevelZero	Agda.TypeChecking.Rules.Builtin
bindBuiltinName	Agda.TypeChecking.Monad.Builtin
bindBuiltinNil	Agda.TypeChecking.Rules.Builtin
bindBuiltinPrimitive	Agda.TypeChecking.Rules.Builtin
bindBuiltinRefl	Agda.TypeChecking.Rules.Builtin
bindBuiltinSharp	Agda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinSuc	Agda.TypeChecking.Rules.Builtin
bindBuiltinSuc'	Agda.TypeChecking.Rules.Builtin
bindBuiltinType	Agda.TypeChecking.Rules.Builtin
bindBuiltinType1	Agda.TypeChecking.Rules.Builtin
bindBuiltinZero	Agda.TypeChecking.Rules.Builtin
bindBuiltinZero'	Agda.TypeChecking.Rules.Builtin
bindConstructor	Agda.TypeChecking.Rules.Builtin
BindHole	Agda.Syntax.Notation
bindLHSVars	Agda.TypeChecking.Rules.LHS
bindModule	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindName	Agda.Syntax.Scope.Monad
bindParameters	Agda.TypeChecking.Rules.Data
bindPostulate	Agda.TypeChecking.Rules.Builtin
bindPostulatedName	Agda.TypeChecking.Rules.Builtin
bindPrimitive	Agda.TypeChecking.Monad.Builtin
bindQModule	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindToConcrete	Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
bindVariable	Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
binop	Agda.Syntax.Concrete.Operators.Parser
Blind
1 (Data Constructor)	Agda.Utils.QuickCheck
2 (Type/Class)	Agda.Utils.QuickCheck
BlkInfo	Agda.Auto.NarrowingSearch
Block	Agda.TypeChecking.Coverage.Match
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.TypeChecking.Level
blockingMeta	Agda.Syntax.Internal
blockOfLines	Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop
blockTerm	Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
bltQual	Agda.Compiler.MAlonzo.Misc
bltQual'	Agda.Compiler.MAlonzo.Primitives
BName	Agda.Syntax.Concrete
bnameFixity	Agda.Syntax.Concrete
Body	Agda.Syntax.Internal
bol	Agda.Syntax.Parser.Lexer
boolPrimTF	Agda.Compiler.Epic.Primitive
boolSemiring	Agda.Termination.Semiring
BothWithAndRHS	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
Bound	Agda.Interaction.Highlighting.Precise
BoundName	Agda.Syntax.Concrete
boundName	Agda.Syntax.Concrete
braces
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
braces'	Agda.Syntax.Concrete.Pretty
bracket	Agda.Utils.Monad
brackets
1 (Function)	Agda.Utils.Pretty
2 (Function)	Agda.TypeChecking.Pretty
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
buildList	Agda.TypeChecking.Primitive
buildMPatterns	Agda.TypeChecking.Coverage.Match
buildOccurrenceGraph	Agda.TypeChecking.Positivity
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
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
builtinArg	Agda.TypeChecking.Monad.Builtin
builtinArgArg	Agda.TypeChecking.Monad.Builtin
builtinBool	Agda.TypeChecking.Monad.Builtin
builtinChar	Agda.TypeChecking.Monad.Builtin
builtinCons	Agda.TypeChecking.Monad.Builtin
builtinConstructors	Agda.TypeChecking.Rules.Builtin
builtinDatatypes	Agda.TypeChecking.Rules.Builtin
builtinEquality	Agda.TypeChecking.Monad.Builtin
builtinFalse	Agda.TypeChecking.Monad.Builtin
builtinFlat	Agda.TypeChecking.Monad.Builtin
builtinFloat	Agda.TypeChecking.Monad.Builtin
builtinInf	Agda.TypeChecking.Monad.Builtin
BuiltinInParameterisedModule	Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinInteger	Agda.TypeChecking.Monad.Builtin
builtinIO	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
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
builtinPostulates	Agda.TypeChecking.Rules.Builtin
BuiltinPragma
1 (Data Constructor)	Agda.Syntax.Concrete
2 (Data Constructor)	Agda.Syntax.Abstract
builtinPrimitives	Agda.TypeChecking.Rules.Builtin
builtinQName	Agda.TypeChecking.Monad.Builtin
builtinRefl	Agda.TypeChecking.Monad.Builtin
builtinSharp	Agda.TypeChecking.Monad.Builtin
builtinSize	Agda.TypeChecking.Monad.Builtin
builtinSizeInf	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
builtinTypes	Agda.TypeChecking.Monad.Builtin
builtinZero	Agda.TypeChecking.Monad.Builtin