Index - B
| B | Agda.Utils.Map |
| Backend | |
| 1 (Type/Class) | Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Compiler.Backend |
| Backend' | |
| 1 (Type/Class) | Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.Compiler.Backend |
| backendInteraction | Agda.Compiler.Backend |
| BackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| backendName | Agda.Compiler.Backend |
| backendUsage | Agda.Main |
| backendVersion | Agda.Compiler.Backend |
| Background | Agda.Interaction.Highlighting.Precise |
| backupPos | Agda.Syntax.Position |
| BadArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BadImplicits | Agda.TypeChecking.Implicit |
| BadMacroDef | Agda.Syntax.Concrete.Definitions |
| BadVisibility | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Bag | |
| 1 (Type/Class) | Agda.Utils.Bag |
| 2 (Data Constructor) | Agda.Utils.Bag |
| bag | Agda.Utils.Bag |
| BDecls | Agda.Utils.Haskell.Syntax |
| begin | Agda.Syntax.Parser.LexActions |
| Beginning | Agda.Syntax.Common |
| beginningOf | Agda.Syntax.Position |
| beginningOfFile | Agda.Syntax.Position |
| beginWith | Agda.Syntax.Parser.LexActions |
| begin_ | Agda.Syntax.Parser.LexActions |
| below | Agda.Utils.IntSet.Infinite |
| Benchmark | |
| 1 (Type/Class) | Agda.Utils.Benchmark |
| 2 (Data Constructor) | Agda.Utils.Benchmark |
| 3 (Type/Class) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| BenchmarkOff | Agda.Utils.Benchmark |
| BenchmarkOn | |
| 1 (Type/Class) | Agda.Utils.Benchmark |
| 2 (Data Constructor) | Agda.Utils.Benchmark |
| benchmarkOn | Agda.Utils.Benchmark |
| benchmarks | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| BenchmarkSome | Agda.Utils.Benchmark |
| bestConInfo | Agda.Syntax.Common |
| betareduce | Agda.Auto.CaseSplit |
| between | Agda.Utils.Parser.ReadP |
| billPureTo | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| billTo | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| billToCPS | 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 | |
| 1 (Function) | Agda.TypeChecking.Free.Lazy |
| 2 (Function) | Agda.TypeChecking.Names |
| bind' | |
| 1 (Function) | Agda.TypeChecking.Free.Lazy |
| 2 (Function) | Agda.TypeChecking.Names |
| 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 |
| Binder | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base |
| 2 (Type/Class) | Agda.Compiler.Treeless.Subst |
| 3 (Data Constructor) | Agda.Compiler.Treeless.Subst |
| bindGeneralizedParameters | Agda.TypeChecking.Rules.Data |
| BindHole | Agda.Syntax.Notation |
| bindModule | Agda.Syntax.Scope.Monad |
| BindName | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| bindName | Agda.Syntax.Scope.Monad |
| bindName' | Agda.Syntax.Scope.Monad |
| bindP | Agda.Utils.Parser.MemoisedCPS |
| bindParameter | Agda.TypeChecking.Rules.Data |
| bindParameters | Agda.TypeChecking.Rules.Data |
| bindPostulatedName | Agda.TypeChecking.Rules.Builtin |
| bindPrimitive | Agda.TypeChecking.Monad.Builtin |
| bindQModule | Agda.Syntax.Scope.Monad |
| bindReduce | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Binds | Agda.Utils.Haskell.Syntax |
| bindsToTel | Agda.TypeChecking.Substitute |
| bindsToTel' | Agda.TypeChecking.Substitute |
| bindTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| bindToConcrete | Agda.Syntax.Translation.AbstractToConcrete |
| bindUntypedBuiltin | Agda.TypeChecking.Rules.Builtin |
| bindVariable | Agda.Syntax.Scope.Monad |
| bindVarsToBind | Agda.Syntax.Scope.Monad |
| BinOp | Agda.Compiler.JS.Syntax |
| 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, Agda.Compiler.Backend |
| BlockedLevel | Agda.Syntax.Internal |
| BlockedOnApply | Agda.TypeChecking.Coverage.Match |
| BlockedOnMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BlockedOnProj | Agda.TypeChecking.Coverage.Match |
| BlockedOnResult | Agda.TypeChecking.Coverage.Match |
| blockedOnResult | Agda.TypeChecking.Coverage.Match |
| blockedOnResultIApply | Agda.TypeChecking.Coverage.Match |
| blockedOnResultOverlap | Agda.TypeChecking.Coverage.Match |
| blockedOnVars | Agda.TypeChecking.Coverage.Match |
| blockedOrMeta | Agda.TypeChecking.Reduce |
| 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 |
| blockingVarLits | Agda.TypeChecking.Coverage.Match |
| blockingVarNo | Agda.TypeChecking.Coverage.Match |
| blockingVarOverlap | Agda.TypeChecking.Coverage.Match |
| BlockingVars | Agda.TypeChecking.Coverage.Match |
| blockOfLines | Agda.Syntax.Scope.Base |
| 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 |
| bol | Agda.Syntax.Parser.Lexer |
| boldPathView | Agda.TypeChecking.Monad.Builtin |
| boolSemiring | Agda.Termination.Semiring |
| boolSing | Agda.Utils.TypeLits |
| boolToMaybe | Agda.Utils.Maybe |
| boolVal | Agda.Utils.TypeLits |
| bothAbsurd | Agda.TypeChecking.Conversion |
| BothWithAndRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| botVarOcc | Agda.TypeChecking.Free.Lazy |
| Bound | |
| 1 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| Boundary | Agda.TypeChecking.Telescope |
| Boundary' | Agda.TypeChecking.Telescope |
| BoundedLt | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BoundedNo | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BoundedSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| boundedSizeMetaHook | Agda.TypeChecking.SizedTypes |
| 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 |
| boundToEverySome | Agda.TypeChecking.Positivity.Occurrence |
| br | Agda.Compiler.JS.Pretty |
| braces | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| braces' | Agda.Syntax.Concrete.Pretty |
| bracesAndSemicolons | Agda.Syntax.Concrete.Pretty |
| brackets | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| bracket_ | Agda.Utils.Monad |
| Branches | Agda.TypeChecking.CompiledClause |
| buildClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| buildConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| buildGraph | Agda.Utils.Warshall |
| BuildInterface | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| buildInterface | Agda.Interaction.Imports |
| buildList | Agda.TypeChecking.Primitive |
| buildOccurrenceGraph | Agda.TypeChecking.Positivity |
| buildProblemConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| buildProblemConstraint_ | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| buildSubstitution | Agda.TypeChecking.Patterns.Match |
| buildWithFunction | Agda.TypeChecking.With |
| Builtin | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinAbs | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAbsAbs | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaClause | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaClauseAbsurd | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaClauseClause | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinition | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionDataConstructor | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionDataDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionFunDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionPostulate | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionPrimitive | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaDefinitionRecordDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaErrorPart | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaErrorPartName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaErrorPartString | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaErrorPartTerm | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitChar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLiteral | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitMeta | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitQName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitString | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaLitWord64 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaMeta | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatAbsurd | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatCon | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatDot | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatLit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatProj | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPattern | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaPatVar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaSort | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaSortLit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaSortSet | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaSortUnsupported | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCM | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMBind | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMBlockOnMeta | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMCatchError | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMCheckType | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMCommit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMDebugPrint | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMDeclareDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMDeclarePostulate | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMDefineFun | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMExtendContext | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMFreshName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMGetContext | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMGetDefinition | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMGetType | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMInContext | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMInferType | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMIsMacro | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMNoConstraints | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMNormalise | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMQuoteTerm | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMReduce | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMReturn | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMRunSpeculative | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMTypeError | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMUnify | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMUnquoteTerm | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTCMWithNormalisation | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTerm | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermCon | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermExtLam | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermLam | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermLit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermMeta | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermPi | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermSort | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermUnsupported | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermVar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinArg | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinArgArg | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinArgArgInfo | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinArgInfo | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAssoc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAssocLeft | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAssocNon | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinAssocRight | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinBackends | Agda.Main |
| builtinBool | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinChar | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinComp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinConId | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinCons | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BuiltinDataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinDesc | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BuiltinDescriptor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinEquality | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinEquiv | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinEquivFun | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinEquivProof | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFaceForall | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFalse | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFixity | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFixityFixity | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFlat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFloat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFromNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFromNeg | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinFromString | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinGlue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinHComp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinHidden | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinHiding | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinId | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIdElim | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIMax | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIMin | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinINeg | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinInf | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinInfo | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BuiltinInParameterisedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinInstance | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinInteger | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIntegerNegSuc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIntegerPos | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinInterval | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIO | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIOne | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIrrelevant | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIsOne | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIsOne1 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIsOne2 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIsOneEmpty | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinItIsOne | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinIZero | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinKindOfName | Agda.TypeChecking.Rules.Builtin |
| BuiltinKit | |
| 1 (Type/Class) | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| 2 (Data Constructor) | Agda.Compiler.Treeless.EliminateLiteralPatterns |
| builtinLevel | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinLevelKit | Agda.TypeChecking.Level |
| builtinLevelMax | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinLevelSuc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinLevelZero | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinList | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinModules | Agda.Interaction.Options.Lenses |
| builtinModulesWithSafePostulates | Agda.Interaction.Options.Lenses |
| builtinModulesWithUnsafePostulates | Agda.Interaction.Options.Lenses |
| BuiltinMustBeConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinNat | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatDivSucAux | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatEquals | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatLess | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatMinus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatModSucAux | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatPlus | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNatTimes | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinNil | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinNoDefPragma | Agda.Syntax.Abstract |
| builtinPartial | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPartialP | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPath | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPathP | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPathToEquiv | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPOr | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinPostulate | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| BuiltinPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| builtinPrecedence | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPrecRelated | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinPrecUnrelated | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinPrim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinQName | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinRefl | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinRelevance | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinRelevant | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinRewrite | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSetOmega | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSharp | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSigma | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSize | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSizeHook | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinSizeInf | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSizeLt | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSizeMax | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSizeSuc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSizeUniv | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinsNoDef | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinString | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSub | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSubIn | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSubOut | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinSuc | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinTrans | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinTrue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinUnit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinUnitUnit | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| BuiltinUnknown | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| builtinVisible | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinWord64 | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtinZero | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtin_glue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |
| builtin_unglue | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin |