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

Index - B

BAgda.Utils.Map
BackendAgda.Interaction.GhciTop
backupPosAgda.Syntax.Position, Agda.Interaction.GhciTop
BadImplicitsAgda.TypeChecking.Implicit
beginAgda.Syntax.Parser.LexActions
beginningOfAgda.Syntax.Position, Agda.Interaction.GhciTop
beginningOfFileAgda.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
bindBuiltinFlatAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInfAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinNameAgda.TypeChecking.Monad.Builtin
bindBuiltinSharpAgda.TypeChecking.Rules.Builtin.Coinduction
bindExprAgda.Compiler.Epic.CompileState
BindHoleAgda.Syntax.Notation
bindLHSVarsAgda.TypeChecking.Rules.LHS
bindModuleAgda.Syntax.Scope.Monad, Agda.Interaction.GhciTop
bindNameAgda.Syntax.Scope.Monad
bindParametersAgda.TypeChecking.Rules.Data
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.Compiler.JS.Syntax
binop 
1 (Function)Agda.Compiler.JS.Parser
2 (Function)Agda.Syntax.Concrete.Operators.Parser
Blind 
1 (Data Constructor)Agda.Utils.QuickCheck
2 (Type/Class)Agda.Utils.QuickCheck
BlkInfoAgda.Auto.NarrowingSearch
BlockAgda.TypeChecking.Coverage.Match
blockAgda.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
blockedAgda.Syntax.Internal
BlockedConstAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BlockedLevelAgda.Syntax.Internal
blockingMetaAgda.Syntax.Internal
blockOfLinesAgda.Syntax.Scope.Base, Agda.Interaction.GhciTop
blockTermAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
blockTermOnProblemAgda.TypeChecking.MetaVars, Agda.Interaction.GhciTop
bltQualAgda.Compiler.MAlonzo.Misc
bltQual'Agda.Compiler.MAlonzo.Primitives
BNameAgda.Syntax.Concrete
bnameFixityAgda.Syntax.Concrete
BodyAgda.Syntax.Internal
body 
1 (Function)Agda.Compiler.JS.Case
2 (Function)Agda.Compiler.JS.Compiler
bolAgda.Syntax.Parser.Lexer
boolPrimTFAgda.Compiler.Epic.Primitive
boolSemiringAgda.Termination.Semiring
BothWithAndRHSAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BoundAgda.Interaction.Highlighting.Precise
BoundNameAgda.Syntax.Concrete
boundNameAgda.Syntax.Concrete
brAgda.Compiler.JS.Pretty
bracedAgda.Compiler.JS.Parser
bracedBlockAgda.Compiler.JS.Parser
braces 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
braces'Agda.Syntax.Concrete.Pretty
bracketAgda.Utils.Monad
bracketedAgda.Compiler.JS.Parser
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
BranchesAgda.TypeChecking.CompiledClause
brExprAgda.Compiler.Epic.AuxAST
BrIntAgda.Compiler.Epic.AuxAST
brIntAgda.Compiler.Epic.AuxAST
brNameAgda.Compiler.Epic.AuxAST
brTagAgda.Compiler.Epic.AuxAST
brVarsAgda.Compiler.Epic.AuxAST
buildClosureAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
buildConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildGraphAgda.Utils.Warshall
buildInterfaceAgda.Interaction.Imports
buildLambdaAgda.Compiler.Epic.Smashing
buildListAgda.TypeChecking.Primitive
buildMPatternsAgda.TypeChecking.Coverage.Match
buildOccurrenceGraphAgda.TypeChecking.Positivity
buildProblemConstraintAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
buildTermAgda.Compiler.Epic.Forcing
buildWithFunctionAgda.TypeChecking.With
Builtin 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinAgdaDataDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataConstructorAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionFunDefAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPostulateAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPrimitiveAgda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionRecordDefAgda.TypeChecking.Monad.Builtin
builtinAgdaFunDefAgda.TypeChecking.Monad.Builtin
builtinAgdaRecordDefAgda.TypeChecking.Monad.Builtin
builtinAgdaSortAgda.TypeChecking.Monad.Builtin
builtinAgdaSortLitAgda.TypeChecking.Monad.Builtin
builtinAgdaSortSetAgda.TypeChecking.Monad.Builtin
builtinAgdaSortUnsupportedAgda.TypeChecking.Monad.Builtin
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
builtinAgdaTypeAgda.TypeChecking.Monad.Builtin
builtinAgdaTypeElAgda.TypeChecking.Monad.Builtin
builtinArgAgda.TypeChecking.Monad.Builtin
builtinArgArgAgda.TypeChecking.Monad.Builtin
builtinBoolAgda.TypeChecking.Monad.Builtin
builtinCharAgda.TypeChecking.Monad.Builtin
builtinConsAgda.TypeChecking.Monad.Builtin
BuiltinDataAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDataConsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinDescAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinDescriptorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinEqualityAgda.TypeChecking.Monad.Builtin
builtinFalseAgda.TypeChecking.Monad.Builtin
builtinFlatAgda.TypeChecking.Monad.Builtin
builtinFloatAgda.TypeChecking.Monad.Builtin
builtinHiddenAgda.TypeChecking.Monad.Builtin
builtinHidingAgda.TypeChecking.Monad.Builtin
builtinInfAgda.TypeChecking.Monad.Builtin
BuiltinInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinInParameterisedModuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinInstanceAgda.TypeChecking.Monad.Builtin
builtinIntegerAgda.TypeChecking.Monad.Builtin
builtinIOAgda.TypeChecking.Monad.Builtin
builtinIrrelevantAgda.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
builtinNameAgda.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
BuiltinPostulateAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
BuiltinPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
BuiltinPrimAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinQNameAgda.TypeChecking.Monad.Builtin
builtinReflAgda.TypeChecking.Monad.Builtin
builtinRelevanceAgda.TypeChecking.Monad.Builtin
builtinRelevantAgda.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
BuiltinUnknownAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
builtinVisibleAgda.TypeChecking.Monad.Builtin
builtinZeroAgda.TypeChecking.Monad.Builtin