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 |