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

Index - B

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
backendInteractionAgda.Compiler.Backend
BackendNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
backendNameAgda.Compiler.Backend
backendUsageAgda.Main
backendVersionAgda.Compiler.Backend
BackgroundAgda.Interaction.Highlighting.Precise
backupPosAgda.Syntax.Position
BadArgumentsToPatternSynonymAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BadFieldNameAgda.Interaction.Library.Base
BadImplicitsAgda.TypeChecking.Implicit
BadLibraryNameAgda.Interaction.Library.Base
BadMacroDefAgda.Syntax.Concrete.Definitions.Errors
badStepAgda.TypeChecking.Rules.LHS.Unify, Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
BadVisibilityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Bag 
1 (Type/Class)Agda.Utils.Bag
2 (Data Constructor)Agda.Utils.Bag
bagAgda.Utils.Bag
bareNameOfAgda.Syntax.Common
bareNameWithDefaultAgda.Syntax.Common
BDeclsAgda.Utils.Haskell.Syntax
beforeReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
beginAgda.Syntax.Parser.LexActions
BeginningAgda.Syntax.Common
beginningOfAgda.Syntax.Position
beginningOfFileAgda.Syntax.Position
beginWithAgda.Syntax.Parser.LexActions
begin_Agda.Syntax.Parser.LexActions
belowAgda.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
BenchmarkOffAgda.Utils.Benchmark
BenchmarkOn 
1 (Type/Class)Agda.Utils.Benchmark
2 (Data Constructor)Agda.Utils.Benchmark
benchmarkOnAgda.Utils.Benchmark
benchmarksAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
BenchmarkSomeAgda.Utils.Benchmark
BenchPhaseAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
BesideAgda.Compiler.JS.Pretty
bestConInfoAgda.Syntax.Common
betareduceAgda.Auto.CaseSplit
billPureToAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billToAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billToCPSAgda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
billToIOAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
billToPureAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
BiMap 
1 (Type/Class)Agda.Utils.BiMap
2 (Data Constructor)Agda.Utils.BiMap
biMapBackAgda.Utils.BiMap
biMapInvariantAgda.Utils.BiMap
biMapThereAgda.Utils.BiMap
BinAppViewAgda.TypeChecking.EtaContract
binAppViewAgda.TypeChecking.EtaContract
BinaryEncodeAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
bindAgda.TypeChecking.Names
bind'Agda.TypeChecking.Names
bindAsPatternsAgda.TypeChecking.Rules.LHS
bindBuiltinAgda.TypeChecking.Rules.Builtin
bindBuiltinFlatAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinInfAgda.TypeChecking.Rules.Builtin.Coinduction
bindBuiltinNameAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
bindBuiltinNoDefAgda.TypeChecking.Rules.Builtin
bindBuiltinRewriteRelationAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
bindBuiltinSharpAgda.TypeChecking.Rules.Builtin.Coinduction
Binder 
1 (Type/Class)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Concrete
3 (Type/Class)Agda.Syntax.Abstract
4 (Data Constructor)Agda.Syntax.Abstract
5 (Type/Class)Agda.Compiler.Treeless.Subst
6 (Data Constructor)Agda.Compiler.Treeless.Subst
Binder' 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
binderName 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
binderPattern 
1 (Function)Agda.Syntax.Concrete
2 (Function)Agda.Syntax.Abstract
bindGeneralizedParametersAgda.TypeChecking.Rules.Data
BindingSourceAgda.Syntax.Scope.Base
bindModuleAgda.Syntax.Scope.Monad
bindNAgda.TypeChecking.Names
BindName 
1 (Type/Class)Agda.Syntax.Abstract
2 (Data Constructor)Agda.Syntax.Abstract
bindNameAgda.Syntax.Scope.Monad
bindName'Agda.Syntax.Scope.Monad
bindName''Agda.Syntax.Scope.Monad
bindNArgAgda.TypeChecking.Names
bindPAgda.Utils.Parser.MemoisedCPS
bindParameterAgda.TypeChecking.Rules.Data
bindParametersAgda.TypeChecking.Rules.Data
bindPostulatedNameAgda.TypeChecking.Rules.Builtin
bindPrimitiveAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
bindQModuleAgda.Syntax.Scope.Monad
bindReduceAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BindsAgda.Utils.Haskell.Syntax
bindsToTelAgda.TypeChecking.Substitute
bindsToTel'Agda.TypeChecking.Substitute
bindsToTel'1Agda.TypeChecking.Substitute
bindsToTel1Agda.TypeChecking.Substitute
bindTCMTAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
bindToConcreteAgda.Syntax.Translation.AbstractToConcrete
bindUntypedBuiltinAgda.TypeChecking.Rules.Builtin
bindVariableAgda.Syntax.Scope.Monad
bindVarsToBindAgda.Syntax.Scope.Monad
BinOpAgda.Compiler.JS.Syntax
blankNotInScopeAgda.Syntax.Translation.InternalToAbstract
BlkInfoAgda.Auto.NarrowingSearch
Block 
1 (Type/Class)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.TypeChecking.Coverage.Match
blockAgda.Compiler.JS.Pretty
Blocked 
1 (Data Constructor)Agda.Auto.NarrowingSearch
2 (Data Constructor)Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
3 (Type/Class)Agda.Syntax.Internal
blockedAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
Blocked'Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
BlockedConstAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
blockedOnAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
BlockedOnApplyAgda.TypeChecking.Coverage.Match
BlockedOnMetaAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BlockedOnProjAgda.TypeChecking.Coverage.Match
BlockedOnResultAgda.TypeChecking.Coverage.Match
blockedOnResultAgda.TypeChecking.Coverage.Match
blockedOnResultIApplyAgda.TypeChecking.Coverage.Match
blockedOnResultOverlapAgda.TypeChecking.Coverage.Match
blockedOnVarsAgda.TypeChecking.Coverage.Match
BlockedTypeAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Blocked_Agda.Syntax.Internal
blocked_Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
BlockerAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
blockingStatusAgda.Syntax.Internal.Blockers, Agda.Syntax.Internal
BlockingVar 
1 (Type/Class)Agda.TypeChecking.Coverage.Match
2 (Data Constructor)Agda.TypeChecking.Coverage.Match
blockingVarConsAgda.TypeChecking.Coverage.Match
blockingVarLazyAgda.TypeChecking.Coverage.Match
blockingVarLitsAgda.TypeChecking.Coverage.Match
blockingVarNoAgda.TypeChecking.Coverage.Match
blockingVarOverlapAgda.TypeChecking.Coverage.Match
BlockingVarsAgda.TypeChecking.Coverage.Match
blockOfLinesAgda.Syntax.Scope.Base
blockOnErrorAgda.TypeChecking.Conversion
blockOnMetasInAgda.TypeChecking.Rewriting.NonLinPattern
BlockT 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
blockTermAgda.TypeChecking.MetaVars
blockTermOnProblemAgda.TypeChecking.MetaVars
blockTypeOnProblemAgda.TypeChecking.MetaVars
bltQualAgda.Compiler.MAlonzo.Misc
bltQual'Agda.Compiler.MAlonzo.Primitives
BNameAgda.Syntax.Concrete
bnameFixityAgda.Syntax.Concrete
bnameIsFiniteAgda.Syntax.Concrete
bnameTacticAgda.Syntax.Concrete
bolAgda.Syntax.Parser.Lexer
boldPathViewAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BoolAgda.Interaction.JSON
boolSemiringAgda.Termination.Semiring
BoolSetAgda.Utils.BoolSet
boolSingAgda.Utils.TypeLits
boolToMaybeAgda.Utils.Maybe
boolValAgda.Utils.TypeLits
bothAbsurdAgda.TypeChecking.Conversion
BothWithAndRHSAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Bound 
1 (Data Constructor)Agda.Interaction.Highlighting.Precise
2 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
BoundaryAgda.TypeChecking.Telescope
Boundary'Agda.TypeChecking.Telescope
BoundedLtAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
BoundedNoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
BoundedSizeAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
boundedSizeMetaHookAgda.TypeChecking.SizedTypes
BoundNameAgda.Syntax.Concrete
boundNameAgda.Syntax.Concrete
Bounds 
1 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
2 (Data Constructor)Agda.TypeChecking.SizedTypes.WarshallSolver
boundsAgda.TypeChecking.SizedTypes.WarshallSolver
boundToEverySomeAgda.TypeChecking.Positivity.Occurrence
BoundVariablePosition 
1 (Type/Class)Agda.Syntax.Common
2 (Data Constructor)Agda.Syntax.Common
braces 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
braces'Agda.Syntax.Concrete.Glyph, Agda.Syntax.Concrete.Pretty
bracesAndSemicolonsAgda.Syntax.Concrete.Pretty
brackets 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
bracket_Agda.Utils.Monad
BranchesAgda.TypeChecking.CompiledClause
BraveTerm 
1 (Type/Class)Agda.Syntax.Internal
2 (Data Constructor)Agda.Syntax.Internal
break 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
breakAfter 
1 (Function)Agda.Utils.List
2 (Function)Agda.Utils.List1
breakAfter1Agda.Utils.List
buildClosureAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
buildConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
buildEquivAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
buildGraphAgda.Utils.Warshall
BuildInterfaceAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
buildLeftInverseAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
buildListAgda.TypeChecking.Primitive
buildOccurrenceGraphAgda.TypeChecking.Positivity
buildProblemConstraintAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
buildProblemConstraint_Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
buildSubstitutionAgda.TypeChecking.Patterns.Match
buildWithFunctionAgda.TypeChecking.With
Builtin 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinAbsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAbsAbsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaClauseAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaClauseAbsurdAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaClauseClauseAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataConstructorAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionDataDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionFunDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPostulateAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionPrimitiveAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaDefinitionRecordDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartNameAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartPattAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartStringAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaErrorPartTermAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitCharAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLiteralAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitFloatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitMetaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitNatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitQNameAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitStringAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaLitWord64Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaMetaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatAbsurdAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatConAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatDotAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatLitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatProjAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatternAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaPatVarAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortInfAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortLitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortPropAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortPropLitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortSetAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaSortUnsupportedAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMBindAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMBlockOnMetaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCatchErrorAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCheckTypeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMCommitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDebugPrintAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDeclareDataAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDeclareDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDeclarePostulateAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDefineDataAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDefineFunAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMDontReduceDefsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMExecAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMExtendContextAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMFormatErrorPartsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMFreshNameAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetContextAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetDefinitionAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetInstancesAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMGetTypeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMInContextAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMInferTypeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMIsMacroAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMNoConstraintsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMNormaliseAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMOnlyReduceDefsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMQuoteOmegaTermAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMQuoteTermAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMReduceAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMReturnAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMRunSpeculativeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMTypeErrorAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnifyAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMUnquoteTermAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMWithNormalisationAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTCMWithReconsParamsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermConAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermExtLamAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermLamAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermLitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermMetaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermPiAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermSortAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermUnsupportedAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAgdaTermVarAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinArgAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinArgArgAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinArgArgInfoAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinArgInfoAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAssocAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAssocLeftAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAssocNonAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinAssocRightAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinBackendsAgda.Compiler.Builtin
builtinBoolAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinCharAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinCompAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinConIdAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinConsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinDataAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BuiltinDataConsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinDescAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BuiltinDescriptorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinEqualityAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinEquivAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinEquivFunAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinEquivProofAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFaceForallAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFalseAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFixityAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFixityFixityAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFlatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFloatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFromNatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFromNegAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinFromStringAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinGlueAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinHCompAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinHiddenAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinHidingAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIdAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIdElimAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIMaxAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIMinAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinINegAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinInfAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinInfo 
1 (Type/Class)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BuiltinInParameterisedModuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinInstanceAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIntegerAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIntegerNegSucAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIntegerPosAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIntervalAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIntervalUnivAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIOAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIOneAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIrrelevantAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIsOneAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIsOne1Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIsOne2Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIsOneEmptyAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinItIsOneAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinIZeroAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinJustAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinKindOfNameAgda.TypeChecking.Rules.Builtin
BuiltinKit 
1 (Type/Class)Agda.Compiler.Treeless.EliminateLiteralPatterns
2 (Data Constructor)Agda.Compiler.Treeless.EliminateLiteralPatterns
builtinLevelAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinLevelKitAgda.TypeChecking.Level
builtinLevelMaxAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinLevelSucAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinLevelZeroAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinListAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinLockUnivAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinMaybeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinModalityAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinModalityConstructorAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinModulesAgda.Interaction.Options.Lenses
builtinModulesWithSafePostulatesAgda.Interaction.Options.Lenses
builtinModulesWithUnsafePostulatesAgda.Interaction.Options.Lenses
BuiltinMustBeConstructorAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinNameAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinNatAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatDivSucAuxAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatEqualsAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatLessAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatMinusAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatModSucAuxAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatPlusAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNatTimesAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinNilAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinNoDefPragmaAgda.Syntax.Abstract
builtinNothingAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPartialAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPartialPAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPathAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPathPAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPOrAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinPostulateAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
BuiltinPragma 
1 (Data Constructor)Agda.Syntax.Concrete
2 (Data Constructor)Agda.Syntax.Abstract
builtinPrecedenceAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPrecRelatedAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinPrecUnrelatedAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinPrimAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinPropAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinQNameAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinQuantityAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinQuantity0Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinQuantityωAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinReflAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinReflIdAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinRelevanceAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinRelevantAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinRewriteAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinRewriteRelationsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinSetAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSetOmegaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSharpAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSigmaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeHookAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
builtinSizeInfAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeLtAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeMaxAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeSucAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSizeUnivAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinsNoDefAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinSortAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinSSetOmegaAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinStrictSetAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinStringAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSubAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSubInAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSubOutAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinSucAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinThingsAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinTransAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinTranspProofAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinTrueAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinUnitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinUnitUnitAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
BuiltinUnknownAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
builtinVisibleAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinWord64Agda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtinZeroAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtin_glueAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtin_glueUAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtin_unglueAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
builtin_unglueUAgda.Syntax.Builtin, Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
ButLoneAgda.TypeChecking.ProjectionLike