B | Agda.Utils.Map |
Backend | Agda.Interaction.InteractionTop |
backupPos | Agda.Syntax.Position |
BadArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
BadImplicits | Agda.TypeChecking.Implicit |
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 |
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.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 |
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 |
bindVariable | Agda.Syntax.Scope.Monad |
BinOp | Agda.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 |
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 |
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 |
branch | Agda.Compiler.MAlonzo.Compiler |
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 |
buildLambda | Agda.Compiler.Epic.Smashing |
buildList | Agda.TypeChecking.Primitive |
buildMPatterns | Agda.TypeChecking.Coverage.Match |
buildOccurrenceGraph | Agda.TypeChecking.Positivity |
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 |
builtinAgdaClause | Agda.TypeChecking.Monad.Builtin |
builtinAgdaClauseAbsurd | Agda.TypeChecking.Monad.Builtin |
builtinAgdaClauseClause | Agda.TypeChecking.Monad.Builtin |
builtinAgdaDataDef | 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 |
builtinAgdaFunDef | Agda.TypeChecking.Monad.Builtin |
builtinAgdaFunDefCon | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLitChar | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLiteral | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLitFloat | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLitNat | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLitQName | Agda.TypeChecking.Monad.Builtin |
builtinAgdaLitString | 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 |
builtinAgdaRecordDef | Agda.TypeChecking.Monad.Builtin |
builtinAgdaSort | Agda.TypeChecking.Monad.Builtin |
builtinAgdaSortLit | Agda.TypeChecking.Monad.Builtin |
builtinAgdaSortSet | Agda.TypeChecking.Monad.Builtin |
builtinAgdaSortUnsupported | 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 |
builtinAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
builtinAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
builtinAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
builtinAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
builtinAgdaType | Agda.TypeChecking.Monad.Builtin |
builtinAgdaTypeEl | 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 |
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 |
builtinIO | Agda.TypeChecking.Monad.Builtin |
builtinIrrAxiom | Agda.TypeChecking.Monad.Builtin |
builtinIrrelevant | 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 |
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 |
BuiltinUnknown | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
builtinVisible | Agda.TypeChecking.Monad.Builtin |
builtinZero | Agda.TypeChecking.Monad.Builtin |