Agda-2.2.8: A dependently typed functional programming language and proof assistant

Index - B

BAgda.Utils.Map
backupPosAgda.Syntax.Position, Agda.Interaction.GhciTop
BadImplicitsAgda.TypeChecking.Implicit
beginAgda.Syntax.Parser.LexActions
beginningOfAgda.Syntax.Position, Agda.Interaction.GhciTop
begin_Agda.Syntax.Parser.LexActions
betareduceAgda.Auto.CaseSplit
betweenAgda.Utils.ReadP
BinAppViewAgda.TypeChecking.EtaContract
binAppViewAgda.TypeChecking.EtaContract
BindAgda.Syntax.Internal
bindAsPatternsAgda.TypeChecking.Rules.LHS
bindBuiltinAgda.TypeChecking.Rules.Builtin
bindBuiltinBoolAgda.TypeChecking.Rules.Builtin
bindBuiltinConsAgda.TypeChecking.Rules.Builtin
bindBuiltinDummyConstructorAgda.TypeChecking.Rules.Builtin
bindBuiltinEqualityAgda.TypeChecking.Rules.Builtin
bindBuiltinFlatAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInfAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinLevelSucAgda.TypeChecking.Rules.Builtin
bindBuiltinLevelZeroAgda.TypeChecking.Rules.Builtin
bindBuiltinNameAgda.TypeChecking.Monad.Builtin
bindBuiltinNilAgda.TypeChecking.Rules.Builtin
bindBuiltinPrimitiveAgda.TypeChecking.Rules.Builtin
bindBuiltinReflAgda.TypeChecking.Rules.Builtin
bindBuiltinSharpAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinSucAgda.TypeChecking.Rules.Builtin
bindBuiltinSuc'Agda.TypeChecking.Rules.Builtin
bindBuiltinTypeAgda.TypeChecking.Rules.Builtin
bindBuiltinType1Agda.TypeChecking.Rules.Builtin
bindBuiltinZeroAgda.TypeChecking.Rules.Builtin
bindBuiltinZero'Agda.TypeChecking.Rules.Builtin
bindConstructorAgda.TypeChecking.Rules.Builtin
BindHoleAgda.Syntax.Notation
bindLHSVarsAgda.TypeChecking.Rules.LHS
bindModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindNameAgda.Syntax.Scope.Monad
bindParametersAgda.TypeChecking.Rules.Data
bindPostulateAgda.TypeChecking.Rules.Builtin
bindPostulatedNameAgda.TypeChecking.Rules.Builtin
bindPrimitiveAgda.TypeChecking.Monad.Builtin
bindQModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindToConcreteAgda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop
bindVariableAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
binopAgda.Syntax.Concrete.Operators.Parser
Blind 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
BlkInfoAgda.Auto.NarrowingSearch
BlockAgda.TypeChecking.Coverage.Match
Blocked 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Type/Class)Agda.Syntax.Internal
3 (Data Constructor)Agda.Syntax.Internal
blockedAgda.Syntax.Internal
BlockedConstAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BlockedLevelAgda.TypeChecking.Level
blockingMetaAgda.Syntax.Internal
blockOfLinesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
blockTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
bltQualAgda.Compiler.MAlonzo.Misc
bltQual'Agda.Compiler.MAlonzo.Primitives
BNameAgda.Syntax.Concrete
bnameFixityAgda.Syntax.Concrete
BodyAgda.Syntax.Internal
bolAgda.Syntax.Parser.Lexer
boolSemiringAgda.Termination.Semiring
BothWithAndRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BoundAgda.Interaction.Highlighting.Precise
BoundNameAgda.Syntax.Concrete
boundNameAgda.Syntax.Concrete
braces 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
braces'Agda.Syntax.Concrete.Pretty
bracketAgda.Utils.Monad
brackets 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
BranchesAgda.TypeChecking.CompiledClause
buildClosureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
buildConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildGraphAgda.Utils.Warshall
buildInterfaceAgda.Interaction.Imports
buildListAgda.TypeChecking.Primitive
buildMPatternsAgda.TypeChecking.Coverage.Match
buildOccurrenceGraphAgda.TypeChecking.Positivity
buildWithFunctionAgda.TypeChecking.With
Builtin 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinAgdaTermAgda.TypeChecking.Monad.Builtin
builtinAgdaTermConAgda.TypeChecking.Monad.Builtin
builtinAgdaTermDefAgda.TypeChecking.Monad.Builtin
builtinAgdaTermLamAgda.TypeChecking.Monad.Builtin
builtinAgdaTermPiAgda.TypeChecking.Monad.Builtin
builtinAgdaTermSortAgda.TypeChecking.Monad.Builtin
builtinAgdaTermUnsupportedAgda.TypeChecking.Monad.Builtin
builtinAgdaTermVarAgda.TypeChecking.Monad.Builtin
builtinArgAgda.TypeChecking.Monad.Builtin
builtinArgArgAgda.TypeChecking.Monad.Builtin
builtinBoolAgda.TypeChecking.Monad.Builtin
builtinCharAgda.TypeChecking.Monad.Builtin
builtinConsAgda.TypeChecking.Monad.Builtin
builtinConstructorsAgda.TypeChecking.Rules.Builtin
builtinDatatypesAgda.TypeChecking.Rules.Builtin
builtinEqualityAgda.TypeChecking.Monad.Builtin
builtinFalseAgda.TypeChecking.Monad.Builtin
builtinFlatAgda.TypeChecking.Monad.Builtin
builtinFloatAgda.TypeChecking.Monad.Builtin
builtinInfAgda.TypeChecking.Monad.Builtin
BuiltinInParameterisedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinIntegerAgda.TypeChecking.Monad.Builtin
builtinIOAgda.TypeChecking.Monad.Builtin
builtinLevelAgda.TypeChecking.Monad.Builtin
builtinLevelKitAgda.TypeChecking.Level
builtinLevelMaxAgda.TypeChecking.Monad.Builtin
builtinLevelSucAgda.TypeChecking.Monad.Builtin
builtinLevelZeroAgda.TypeChecking.Monad.Builtin
builtinListAgda.TypeChecking.Monad.Builtin
BuiltinMustBeConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinNatAgda.TypeChecking.Monad.Builtin
builtinNatDivSucAuxAgda.TypeChecking.Monad.Builtin
builtinNatEqualsAgda.TypeChecking.Monad.Builtin
builtinNatLessAgda.TypeChecking.Monad.Builtin
builtinNatMinusAgda.TypeChecking.Monad.Builtin
builtinNatModSucAuxAgda.TypeChecking.Monad.Builtin
builtinNatPlusAgda.TypeChecking.Monad.Builtin
builtinNatTimesAgda.TypeChecking.Monad.Builtin
builtinNilAgda.TypeChecking.Monad.Builtin
builtinPostulatesAgda.TypeChecking.Rules.Builtin
BuiltinPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
builtinPrimitivesAgda.TypeChecking.Rules.Builtin
builtinQNameAgda.TypeChecking.Monad.Builtin
builtinReflAgda.TypeChecking.Monad.Builtin
builtinSharpAgda.TypeChecking.Monad.Builtin
builtinSizeAgda.TypeChecking.Monad.Builtin
builtinSizeInfAgda.TypeChecking.Monad.Builtin
builtinSizeSucAgda.TypeChecking.Monad.Builtin
builtinStringAgda.TypeChecking.Monad.Builtin
builtinSucAgda.TypeChecking.Monad.Builtin
BuiltinThingsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinTrueAgda.TypeChecking.Monad.Builtin
builtinTypesAgda.TypeChecking.Monad.Builtin
builtinZeroAgda.TypeChecking.Monad.Builtin