IndexAgda-2.7.0.1
T
- TAgda.Mimer.Options
- TAConAgda.Syntax.Treeless
- TacticAgda.Syntax.Concrete
- TacticAttributeAgda.Syntax.AbstractAgda.Syntax.Concrete
- TacticAttributeAgda.Syntax.ConcreteAgda.Syntax.Concrete.Attribute
- TacticAttribute'Agda.Syntax.Concrete
- TacticAttributeNotAllowedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tacticAttributesAgda.Syntax.Concrete.Attribute
- TagAgda.Utils.BiMap
- tagAgda.Utils.BiMap
- tagFieldNameAgda.Interaction.JSON
- TaggedObjectAgda.Interaction.JSON
- tagInjectiveForAgda.Utils.BiMap
- tagSingleConstructorsAgda.Interaction.JSON
- TAGuardAgda.Syntax.Treeless
- tailAgda.Utils.List1Agda.Utils.List2
- tailMaybeAgda.Utils.List
- tailsAgda.Utils.List1
- tails1Agda.Utils.List1
- tailWithDefaultAgda.Utils.List
- takeAgda.Utils.List1
- takeAwakeConstraintAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- takeAwakeConstraint'Agda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- takeConstraintsAgda.Compiler.BackendAgda.TypeChecking.Monad.Constraints
- takeOptionsPragmasAgda.Syntax.Parser.Helpers
- takePAgda.Utils.Permutation
- takeSizeConstraintsAgda.TypeChecking.SizedTypes
- takeWhileAgda.Utils.List1
- takeWhileJustAgda.Utils.List
- TALitAgda.Syntax.Treeless
- tallyDefAgda.TypeChecking.MetaVars.Occurs
- TAltAgda.Syntax.Treeless
- TAppAgda.Syntax.Treeless
- tAppViewAgda.Syntax.Treeless
- TargetAgda.Termination.Monad
- targetAgda.Termination.CallGraphAgda.Utils.BiMap
- targetAgda.Utils.Graph.AdjacencyMap.Unidirectional
- TargetDefAgda.Termination.Monad
- targetNodesAgda.Termination.CallGraphAgda.Utils.Graph.AdjacencyMap.Unidirectional
- TargetOtherAgda.Termination.Monad
- TargetRecordAgda.Termination.Monad
- tbFiniteAgda.Syntax.Abstract
- TBindAgda.Syntax.AbstractAgda.Syntax.Concrete
- tbTacticAttrAgda.Syntax.Abstract
- TCaseAgda.Syntax.Treeless
- TCEnvAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCEnvAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCErrAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcErrClosErrAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcErrLocationAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcErrStateAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcErrStringAgda.TypeChecking.Errors
- tcExecAgda.TypeChecking.Unquote
- TCMAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCMAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCMErrorAgda.Interaction.ExitCode
- TCMTAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCoerceAgda.Syntax.Treeless
- TConAgda.Syntax.Treeless
- TCStAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCStateAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TCWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningCachedAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningLocationAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningOriginAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningPrintedWarningAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningRangeAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningsAgda.TypeChecking.Warnings
- tcWarningsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- tcWarningsToErrorAgda.TypeChecking.ErrorsAgda.TypeChecking.Pretty.Warning
- TDefAgda.Syntax.Treeless
- TelAgda.Syntax.Concrete.Pretty
- TelAgda.Syntax.Concrete.Pretty
- TeleAgda.Syntax.Internal
- tele2NamedArgsAgda.TypeChecking.Telescope
- teleArgNamesAgda.TypeChecking.Telescope
- teleArgsAgda.TypeChecking.Telescope
- teleDomsAgda.TypeChecking.Telescope
- teleElimsAgda.TypeChecking.Telescope
- teleLamAgda.TypeChecking.Substitute
- teleNamedArgsAgda.TypeChecking.Telescope
- teleNamesAgda.TypeChecking.Telescope
- TeleNoAbsAgda.TypeChecking.Substitute
- teleNoAbsAgda.TypeChecking.Substitute
- telePatternsAgda.TypeChecking.Telescope
- telePatterns'Agda.TypeChecking.Telescope
- telePiAgda.TypeChecking.Substitute
- telePi'Agda.TypeChecking.Substitute
- telePi_Agda.TypeChecking.Substitute
- telePiPathAgda.TypeChecking.Telescope.Path
- telePiPath_Agda.TypeChecking.Telescope.Path
- telePiVisibleAgda.TypeChecking.Substitute
- TelescopeAgda.Syntax.AbstractAgda.Syntax.ConcreteAgda.Syntax.Internal
- Telescope1Agda.Syntax.AbstractAgda.Syntax.Concrete
- telFromListAgda.Syntax.Internal
- telFromList'Agda.Syntax.Internal
- tell1Agda.Utils.Monad
- tellDirtyAgda.Utils.Update
- tellEmacsToJumpToErrorAgda.Interaction.InteractionTop
- tellEqAgda.TypeChecking.Rewriting.NonLinMatch
- tellSubAgda.TypeChecking.Rewriting.NonLinMatch
- tellToUpdateHighlightingAgda.Interaction.InteractionTop
- tellUnifyProofAgda.TypeChecking.Rules.LHS.Unify.Types
- tellUnifySubstAgda.TypeChecking.Rules.LHS.Unify.Types
- TelToArgsAgda.Syntax.Internal
- telToArgsAgda.Syntax.Internal
- telToListAgda.Syntax.Internal
- TelVAgda.TypeChecking.Substitute
- TelVAgda.TypeChecking.Substitute
- telVarsAgda.TypeChecking.Substitute
- TelViewAgda.TypeChecking.Substitute
- telViewAgda.TypeChecking.Telescope
- telView'Agda.TypeChecking.Substitute
- telView'PathAgda.TypeChecking.Telescope
- telView'UpToAgda.TypeChecking.Substitute
- telView'UpToPathAgda.TypeChecking.Telescope
- telViewPathAgda.TypeChecking.Telescope
- telViewPathBoundaryPAgda.TypeChecking.Telescope
- telViewUpToAgda.TypeChecking.Telescope
- telViewUpTo'Agda.TypeChecking.Telescope
- telViewUpToPathAgda.TypeChecking.Telescope
- telViewUpToPathBoundaryAgda.TypeChecking.Telescope
- telViewUpToPathBoundary'Agda.TypeChecking.Telescope
- telViewUpToPathBoundaryPAgda.TypeChecking.Telescope
- TempInstanceTableAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TentativeAgda.Syntax.Parser.Monad
- TErasedAgda.Syntax.Treeless
- terAskAgda.Termination.Monad
- terAsksAgda.Termination.Monad
- terCurrentAgda.Termination.Monad
- terCutOffAgda.Termination.Monad
- TerEnvAgda.Termination.Monad
- TerEnvAgda.Termination.Monad
- terGetCurrentAgda.Termination.Monad
- terGetCutOffAgda.Termination.Monad
- terGetGuardedAgda.Termination.Monad
- terGetHaveInlinedWithAgda.Termination.Monad
- terGetMaskArgsAgda.Termination.Monad
- terGetMaskResultAgda.Termination.Monad
- terGetMutualAgda.Termination.Monad
- terGetPatternsAgda.Termination.Monad
- terGetSharpAgda.Termination.Monad
- terGetSizeSucAgda.Termination.Monad
- terGetTargetAgda.Termination.Monad
- terGetUsableVarsAgda.Termination.Monad
- terGetUseDotPatternsAgda.Termination.Monad
- terGetUserNamesAgda.Termination.Monad
- terGetUseSizeLtAgda.Termination.Monad
- terGuardedAgda.Termination.Monad
- terHaveInlinedWithAgda.Termination.Monad
- terLocalAgda.Termination.Monad
- TerMAgda.Termination.Monad
- TerMAgda.Termination.Monad
- TermAgda.Syntax.InternalAgda.Syntax.Reflected
- terMAgda.Termination.Monad
- terMaskArgsAgda.Termination.Monad
- terMaskResultAgda.Termination.Monad
- termCAgda.TypeChecking.Serialise.Base
- termDAgda.TypeChecking.Serialise.Base
- termDeclAgda.Termination.TermCheck
- termErrCallsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- termErrFunctionsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TermHeadAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- terminatesAgda.Termination.Termination
- terminatesFilterAgda.Termination.Termination
- TerminatingAgda.Syntax.Common
- TerminationAgda.Benchmarking
- TerminationCheckAgda.Syntax.Common
- TerminationCheckAgda.Syntax.Concrete.Definitions.Types
- TerminationCheckAgda.Syntax.Common
- terminationCheckAgda.Syntax.Concrete.Definitions.Types
- TerminationCheckPragmaAgda.Syntax.Concrete
- terminationCheckPragmaAgda.Syntax.Concrete.Definitions.Monad
- TerminationErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TerminationErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TerminationIssueAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TerminationIssue_Agda.Interaction.Options.Warnings
- TerminationMeasureAgda.Syntax.Common
- TerminationProblemAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- TermLikeAgda.Syntax.Internal.Generic
- termMutualAgda.Termination.TermCheck
- terModifyGuardedAgda.Termination.Monad
- terModifyUsableVarsAgda.Termination.Monad
- terModifyUseSizeLtAgda.Termination.Monad
- TermPartAgda.TypeChecking.Unquote
- TermPositionAgda.TypeChecking.Primitive.Cubical.Base
- TermSizeAgda.Syntax.Internal
- termSizeAgda.Syntax.Internal
- termsSAgda.TypeChecking.Rules.LHS.Unify.LeftInverse
- TermSubstAgda.TypeChecking.Substitute.Class
- TermToPatternAgda.TypeChecking.Patterns.Internal
- termToPatternAgda.TypeChecking.Patterns.Internal
- terMutualAgda.Termination.Monad
- terPatternsAgda.Termination.Monad
- terPatternsRaiseAgda.Termination.Monad
- terRaiseAgda.Termination.Monad
- TErrorAgda.Syntax.Treeless
- TErrorAgda.Syntax.Treeless
- terSetCurrentAgda.Termination.Monad
- terSetGuardedAgda.Termination.Monad
- terSetHaveInlinedWithAgda.Termination.Monad
- terSetMaskArgsAgda.Termination.Monad
- terSetMaskResultAgda.Termination.Monad
- terSetPatternsAgda.Termination.Monad
- TerSetSizeDepthAgda.Termination.Monad
- terSetSizeDepthAgda.Termination.Monad
- terSetTargetAgda.Termination.Monad
- terSetUsableVarsAgda.Termination.Monad
- terSetUseDotPatternsAgda.Termination.Monad
- terSetUseSizeLtAgda.Termination.Monad
- terSharpAgda.Termination.Monad
- terSizeDepthAgda.Termination.Monad
- terSizeSucAgda.Termination.Monad
- terTargetAgda.Termination.Monad
- terUnguardedAgda.Termination.Monad
- terUsableVarsAgda.Termination.Monad
- terUseDotPatternsAgda.Termination.Monad
- terUserNamesAgda.Termination.Monad
- terUseSizeLtAgda.Termination.Monad
- testLubAgda.TypeChecking.SizedTypes.WarshallSolver
- testSuccsAgda.TypeChecking.SizedTypes.WarshallSolver
- TexFileTypeAgda.Syntax.Common
- textAgda.Compiler.JS.PrettyAgda.Syntax.Common.PrettyAgda.TypeChecking.Pretty
- textPathAgda.Utils.FileName
- tgtNodesAgda.Utils.Graph.AdjacencyMap.Unidirectional
- thd3Agda.Utils.Tuple
- theAttrAgda.Syntax.Parser.Helpers
- theBenchmarkAgda.Compiler.BackendAgda.TypeChecking.Monad.State
- theBlockerAgda.Syntax.Internal.Blockers
- theCallGraphAgda.Termination.CallGraph
- theConstraintAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- theCoreAgda.TypeChecking.Substitute
- theCurrentFileAgda.Interaction.Base
- theDefAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- theEtaEqualityAgda.Compiler.BackendAgda.Compiler.BackendAgda.TypeChecking.Monad.BaseAgda.TypeChecking.Monad.Base
- theFixityAgda.Syntax.Common
- TheFlexRigMapAgda.TypeChecking.Free.Lazy
- theFlexRigMapAgda.TypeChecking.Free.Lazy
- TheInfoAgda.TypeChecking.Coverage.SplitClause
- theInteractionPointsAgda.Interaction.Base
- theKindAgda.Syntax.Scope.Base
- theMetaSetAgda.TypeChecking.Free.Lazy
- theNameRangeAgda.Syntax.Common
- theNotationAgda.Syntax.Common
- thenReduceAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- thenTCMTAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- theSizeAgda.Utils.Size
- theSmallSetAgda.Utils.SmallSet
- theSolutionAgda.TypeChecking.SizedTypes.Syntax
- theTacticAttributeAgda.Syntax.Concrete
- theTelAgda.TypeChecking.Substitute
- TheVarMapAgda.TypeChecking.Free.Lazy
- theVarMapAgda.TypeChecking.Free.Lazy
- TheVarMap'Agda.TypeChecking.Free.Lazy
- ThingsInScopeAgda.Syntax.Scope.Base
- thingsInScopeAgda.Syntax.Scope.Base
- ThingWithFixityAgda.Syntax.ConcreteAgda.Syntax.Fixity
- ThingWithFixityAgda.Syntax.ConcreteAgda.Syntax.Fixity
- ThreeAgda.Utils.Three
- ThreeAgda.Utils.Three
- throwDecodeAgda.Interaction.JSON
- throwDecode'Agda.Interaction.JSON
- throwDecodeStrictAgda.Interaction.JSON
- throwDecodeStrict'Agda.Interaction.JSON
- throwDecodeStrictTextAgda.Interaction.JSON
- throwImpossibleAgda.Utils.Impossible
- throwMultipleFixityDeclsAgda.Syntax.Concrete.Fixity
- throwMultiplePolarityPragmasAgda.Syntax.Concrete.Fixity
- tickAgda.Compiler.BackendAgda.TypeChecking.Monad.Statistics
- tickICodeAgda.TypeChecking.Serialise.Base
- tickMaxAgda.Compiler.BackendAgda.TypeChecking.Monad.Statistics
- tickNAgda.Compiler.BackendAgda.TypeChecking.Monad.Statistics
- tIfThenElseAgda.Syntax.Treeless
- TimingsAgda.Utils.Benchmark
- timingsAgda.Utils.Benchmark
- tIntAgda.Syntax.Treeless
- TLamAgda.Syntax.Treeless
- tLamViewAgda.Syntax.Treeless
- TLetAgda.Syntax.AbstractAgda.Syntax.ConcreteAgda.Syntax.Treeless
- tLetViewAgda.Syntax.Treeless
- tLevelUnivAgda.TypeChecking.Primitive.Base
- TLitAgda.Syntax.Treeless
- tlmodOfAgda.Compiler.MAlonzo.Misc
- tMaybeAgda.TypeChecking.Primitive.Base
- TMetaAgda.Syntax.Treeless
- tmSortAgda.Syntax.Internal
- tmSSortAgda.Syntax.Internal
- tNegPlusKAgda.Syntax.Treeless
- toAgda.Interaction.Highlighting.Range
- toAbsNAgda.TypeChecking.Names
- toAbsNameAgda.TypeChecking.Serialise.Instances.Abstract
- ToAbstractAgda.Syntax.Translation.ConcreteToAbstractAgda.Syntax.Translation.ReflectedToAbstract
- toAbstractAgda.Syntax.Translation.ConcreteToAbstractAgda.Syntax.Translation.ReflectedToAbstract
- toAbstract_Agda.Syntax.Translation.ReflectedToAbstract
- toAbstractWithoutImplicitAgda.Syntax.Translation.ReflectedToAbstract
- ToArgsAgda.Interaction.JSON
- toAscListAgda.Utils.BagAgda.Utils.BoolSetAgda.Utils.SmallSetAgda.Utils.Trie
- toAtomsAgda.Interaction.Highlighting.Common
- toAttributeAgda.Syntax.Parser.Helpers
- toBoolAgda.Utils.Boolean
- ToConcreteAgda.Syntax.Translation.AbstractToConcrete
- toConcreteAgda.Syntax.Translation.AbstractToConcrete
- toConcreteCtxAgda.Syntax.Translation.AbstractToConcrete
- toConPatternInfoAgda.Syntax.Internal
- toCTypeAgda.TypeChecking.Primitive.Cubical
- toDescListAgda.Utils.VarSet
- toDistinctAscendingListsAgda.Utils.BiMap
- toEncodingAgda.Interaction.JSON
- toEncoding1Agda.Interaction.JSON
- toEncoding2Agda.Interaction.JSON
- toEncodingListAgda.Interaction.JSON
- toExpandLastAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- toFiniteListAgda.Utils.IntSet.Infinite
- toFinitePiAgda.TypeChecking.Primitive.Base
- ToggleImplicitArgsAgda.Interaction.Base
- ToggleIrrelevantArgsAgda.Interaction.Base
- toIFileAgda.Interaction.FindFile
- toImpossibleAgda.Utils.Empty
- ToJSONAgda.Interaction.JSON
- toJSONAgda.Interaction.JSON
- ToJSON1Agda.Interaction.JSON
- toJSON1Agda.Interaction.JSON
- ToJSON2Agda.Interaction.JSON
- toJSON2Agda.Interaction.JSON
- ToJSONKeyAgda.Interaction.JSON
- toJSONKeyAgda.Interaction.JSON
- ToJSONKeyFunctionAgda.Interaction.JSON
- toJSONKeyListAgda.Interaction.JSON
- ToJSONKeyTextAgda.Interaction.JSON
- ToJSONKeyValueAgda.Interaction.JSON
- toJSONListAgda.Interaction.JSON
- tokAgda.Utils.Parser.MemoisedCPS
- TokCommentAgda.Syntax.Parser.Tokens
- TokDummyAgda.Syntax.Parser.Tokens
- TokenAgda.Mimer.OptionsAgda.Syntax.Parser.Tokens
- tokenAgda.Syntax.Parser.LexActionsAgda.Utils.Parser.MemoisedCPS
- TokenBasedAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- TokenBasedAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- tokenBasedAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- TokenLengthAgda.Syntax.Parser.Alex
- tokensParserAgda.Syntax.ParserAgda.Syntax.Parser.Parser
- TokEOFAgda.Syntax.Parser.Tokens
- TokIdAgda.Syntax.Parser.Tokens
- TokKeywordAgda.Syntax.Parser.Tokens
- TokLiteralAgda.Syntax.Parser.Tokens
- TokMarkupAgda.Syntax.Parser.Tokens
- TokQIdAgda.Syntax.Parser.Tokens
- TokStringAgda.Syntax.Parser.Tokens
- TokSymbolAgda.Syntax.Parser.Tokens
- TokTeXAgda.Syntax.Parser.Tokens
- toLazyAgda.Utils.Maybe.Strict
- toListAgda.Utils.List2
- toListAgda.Termination.CallGraphAgda.Termination.CallMatrixAgda.Utils.BagAgda.Utils.BiMapAgda.Utils.BoolSetAgda.Utils.HashTableAgda.Utils.SmallSetAgda.Utils.TrieAgda.Utils.VarSet
- toListAgda.Interaction.Highlighting.PreciseAgda.Utils.FavoritesAgda.Utils.List1Agda.Utils.RangeMap
- toList'Agda.Utils.List1
- toList1Agda.Utils.List2
- toList1EitherAgda.Utils.List2
- toListOrderedByAgda.Utils.Trie
- toListsAgda.Termination.SparseMatrix
- toLTypeAgda.TypeChecking.Primitive.Cubical
- toMapAgda.Interaction.Highlighting.PreciseAgda.Utils.RangeMap
- ToNLPatAgda.TypeChecking.Rewriting.Clause
- toNLPatAgda.TypeChecking.Rewriting.Clause
- TooFewArgumentsToPatternSynonymAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TooManyArgumentsToLeveledSortAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TooManyArgumentsToUnivOmegaAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TooManyFieldsAgda.Compiler.BackendAgda.TypeChecking.Monad.BaseAgda.TypeChecking.Monad.Base.Warning
- TooManyFields_Agda.Interaction.Options.Warnings
- TooManyPolaritiesAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- toOrderingsAgda.Utils.PartialOrd
- TopAgda.TypeChecking.SizedTypes.Utils
- tOpAgda.Syntax.Treeless
- topAgda.TypeChecking.SizedTypes.Utils
- topBlockAgda.Syntax.Parser.Monad
- topCohesionAgda.Syntax.Common
- TopCtxAgda.Syntax.Fixity
- TopKAgda.Syntax.Concrete.Operators.Parser.Monad
- TopLevelAgda.Syntax.Translation.ConcreteToAbstract
- TopLevelAgda.Syntax.Translation.ConcreteToAbstract
- topLevelArgAgda.TypeChecking.Injectivity
- topLevelDeclsAgda.Syntax.Translation.ConcreteToAbstract
- topLevelExpectedNameAgda.Syntax.Translation.ConcreteToAbstract
- TopLevelInfoAgda.Syntax.Translation.ConcreteToAbstract
- TopLevelInfoAgda.Syntax.Translation.ConcreteToAbstract
- topLevelModuleDropperAgda.TypeChecking.Errors
- TopLevelModuleNameAgda.Syntax.TopLevelModuleName
- TopLevelModuleNameAgda.Syntax.TopLevelModuleName.Boot
- topLevelModuleNameAgda.Compiler.BackendAgda.Compiler.CommonAgda.Syntax.Translation.ConcreteToAbstractAgda.TypeChecking.Monad.State
- TopLevelModuleName'Agda.Syntax.TopLevelModuleName.Boot
- TopLevelModuleNamePartsAgda.Syntax.TopLevelModuleName.Boot
- topLevelModuleNameToQNameAgda.Syntax.TopLevelModuleName
- topLevelPathAgda.Syntax.Translation.ConcreteToAbstract
- topLevelScopeAgda.Syntax.Translation.ConcreteToAbstract
- topLevelTheThingAgda.Syntax.Translation.ConcreteToAbstract
- topModalityAgda.Syntax.Common
- TopModuleAgda.Benchmarking
- TopOpenModuleAgda.Syntax.Scope.Monad
- topoSortAgda.Utils.Permutation
- topoSortMAgda.Utils.Permutation
- topQuantityAgda.Syntax.Common
- topRelevanceAgda.Syntax.Common
- topSortAgda.Utils.Graph.TopSort
- topVarOccAgda.TypeChecking.Free.Lazy
- toReduceDefsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- toSingletonAgda.Utils.BoolSet
- toSparseRowsAgda.Termination.SparseMatrix
- toSplitPatternsAgda.TypeChecking.Coverage.Match
- toSplitPSubstAgda.TypeChecking.Coverage.Match
- toStrictAgda.Utils.Maybe.Strict
- toStringWithoutDotZeroAgda.Utils.Float
- toSubscriptDigitAgda.Utils.Suffix
- totalAgda.Utils.BoolSetAgda.Utils.SmallSet
- ToTermAgda.TypeChecking.Primitive
- toTermAgda.TypeChecking.Primitive
- toTermRAgda.TypeChecking.Primitive
- toTreeAgda.TypeChecking.Coverage.SplitTree
- toTreelessAgda.Compiler.BackendAgda.Compiler.ToTreeless
- toTreelessWithAgda.Compiler.ToTreeless
- toTreesAgda.TypeChecking.Coverage.SplitTree
- toVimAgda.Interaction.Highlighting.Vim
- toWeightAgda.TypeChecking.SizedTypes.WarshallSolver
- TPFnAgda.Syntax.Treeless
- tPlusKAgda.Syntax.Treeless
- TPOpAgda.Syntax.Treeless
- TPrimAgda.Syntax.Treeless
- TPrimAgda.Syntax.Treeless
- traceAgda.TypeChecking.SizedTypes.Utils
- traceCallAgda.Compiler.BackendAgda.TypeChecking.Monad.Trace
- traceCallCPSAgda.Compiler.BackendAgda.TypeChecking.Monad.Trace
- traceCallMAgda.Compiler.BackendAgda.TypeChecking.Monad.Trace
- traceClosureCallAgda.Compiler.BackendAgda.TypeChecking.Monad.Trace
- traceDebugMessageAgda.Compiler.BackendAgda.TypeChecking.Monad.Debug
- traceMAgda.TypeChecking.SizedTypes.Utils
- TraceSAgda.Compiler.BackendAgda.TypeChecking.Monad.Debug
- traceSAgda.Compiler.BackendAgda.TypeChecking.Monad.Debug
- traceSDocAgda.Compiler.BackendAgda.TypeChecking.Monad.Debug
- traceSLnAgda.Compiler.BackendAgda.TypeChecking.Monad.Debug
- trailingWithPatternsAgda.Syntax.Abstract.Pattern
- trampolineAgda.Utils.Function
- trampolineMAgda.Utils.Function
- trampolineWhileAgda.Utils.Function
- trampolineWhileMAgda.Utils.Function
- transClosAgda.TypeChecking.SizedTypes.WarshallSolver
- transformAgda.Compiler.Treeless.EliminateLiteralPatterns
- transitiveClosureAgda.Utils.Graph.AdjacencyMap.Unidirectional
- transitiveReductionAgda.Utils.Graph.AdjacencyMap.Unidirectional
- translateBuiltinsAgda.Compiler.Treeless.Builtin
- translateCompiledClausesAgda.TypeChecking.RecordPatterns
- translateRecordPatternsAgda.TypeChecking.RecordPatterns
- translateSplitTreeAgda.TypeChecking.RecordPatterns
- TransparentDefAgda.Syntax.Common
- TranspErrorAgda.TypeChecking.Primitive.Cubical
- TranspOpAgda.TypeChecking.Primitive.Cubical.Base
- transposeAgda.Termination.SparseMatrix
- transposeAgda.Utils.Graph.AdjacencyMap.UnidirectionalAgda.Utils.List1
- transposeEdgeAgda.Utils.Graph.AdjacencyMap.Unidirectional
- transpPathPTel'Agda.TypeChecking.Primitive.Cubical
- transpPathTel'Agda.TypeChecking.Primitive.Cubical
- transpSysAgda.TypeChecking.Primitive.Cubical
- transpSysTel'Agda.TypeChecking.Primitive.Cubical
- transpTelAgda.TypeChecking.Primitive.Cubical
- transpTel'Agda.TypeChecking.Primitive.Cubical
- traverse'Agda.Utils.Bag
- traverseAPatternMAgda.Syntax.Abstract.Pattern
- traverseArray_Agda.Utils.IArray
- traverseCPatternAAgda.Syntax.Concrete.Pattern
- traverseCPatternMAgda.Syntax.Concrete.Pattern
- TraverseDeclAgda.Syntax.Concrete.Generic
- traverseEitherAgda.Utils.Either
- traverseExprAgda.Syntax.Abstract.ViewsAgda.Syntax.Concrete.Generic
- TraverseExprFnAgda.Syntax.Abstract.Views
- TraverseExprRecFnAgda.Syntax.Abstract.Views
- traverseFAgda.Utils.Functor
- traversePatternMAgda.Syntax.Internal.Pattern
- traverseTermMAgda.Syntax.Internal.Generic
- treelessPrimNameAgda.Compiler.MAlonzo.Primitives
- trFillPathPTel'Agda.TypeChecking.Primitive.Cubical
- trFillPathTel'Agda.TypeChecking.Primitive.Cubical
- trFillTelAgda.TypeChecking.Primitive.Cubical
- trFillTel'Agda.TypeChecking.Primitive.Cubical
- TrieAgda.Utils.Trie
- TrieAgda.Utils.Trie
- TriedToCopyConstrainedPrimAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- trimAgda.Utils.String
- trimLineCommentAgda.Interaction.Library.Parse
- trivialAgda.TypeChecking.SizedTypes
- trueAgda.Utils.Boolean
- trueConditionAgda.TypeChecking.MetaVars
- truncatedCallStackAgda.Utils.CallStack
- TruncateOffsetAgda.TypeChecking.SizedTypes.Syntax
- truncateOffsetAgda.TypeChecking.SizedTypes.Syntax
- tryAddBoundaryAgda.TypeChecking.MetaVars
- tryCatchAgda.Utils.Monad
- tryConversionAgda.TypeChecking.Conversion
- tryConversion'Agda.TypeChecking.Conversion
- tryGetOpenAgda.Compiler.BackendAgda.TypeChecking.Monad.Open
- tryMaybeAgda.Utils.Monad
- tryRecordTypeAgda.TypeChecking.Records
- tryResolveNameAgda.Syntax.Scope.Monad
- trySizeUnivAgda.TypeChecking.SizedTypes
- tryStrengthenAgda.Compiler.Treeless.Subst
- tryTranspErrorAgda.TypeChecking.Primitive.Cubical
- tsetAgda.TypeChecking.Primitive.Base
- tsizeAgda.Syntax.Internal
- tSizeUnivAgda.TypeChecking.Primitive.Base
- TSortAgda.Syntax.Treeless
- TTermAgda.Syntax.Treeless
- TUnitAgda.Syntax.Treeless
- TUnreachableAgda.Syntax.Treeless
- tUnreachableAgda.Syntax.Treeless
- TVarAgda.Syntax.Treeless
- TwoAgda.Utils.Three
- TwoElemArrayAgda.Interaction.JSON
- TyAppAgda.Utils.Haskell.Syntax
- TyConAgda.Utils.Haskell.Syntax
- TyForallAgda.Utils.Haskell.Syntax
- TyFunAgda.Utils.Haskell.Syntax
- TypeAgda.Utils.Haskell.Syntax
- TypeAgda.Syntax.AbstractAgda.Syntax.InternalAgda.Syntax.Reflected
- TypeAgda.Syntax.Internal
- Type'Agda.Syntax.Internal
- Type''Agda.Syntax.Internal
- typeAndFacesInMetaAgda.Interaction.BasicOps
- typeAnnotationsAgda.TypeChecking.Rules.LHS.Problem
- typeArgsWithTelAgda.TypeChecking.Substitute
- typeArityAgda.TypeChecking.Telescope
- TypeCheckAgda.Interaction.Imports
- TypeCheckActionAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TypeCheckingProblemAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeCheckMainAgda.Interaction.Imports
- TypeChecksAgda.Interaction.Highlighting.PreciseAgda.Syntax.Common.Aspect
- TypeclassAgda.Benchmarking
- typeConArgsLeftAgda.TypeChecking.Rules.LHS.Unify.Types
- typeConArgsRightAgda.TypeChecking.Rules.LHS.Unify.Types
- typeConInjectAtAgda.TypeChecking.Rules.LHS.Unify.Types
- TypeConInjectivityAgda.TypeChecking.Rules.LHS.Unify.Types
- typeConstructorAgda.TypeChecking.Rules.LHS.Unify.Types
- TypedAssignAgda.Interaction.Base
- TypedBindingAgda.Syntax.Abstract
- TypedBindingAgda.Syntax.Concrete
- TypedBinding'Agda.Syntax.Concrete
- TypedBindingInfoAgda.Syntax.Abstract
- TypedBindingInfoAgda.Syntax.Abstract
- TypeDeclAgda.Utils.Haskell.Syntax
- TypeDoesNotEndInSortAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeElimsAgda.TypeChecking.Records
- TypeErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- TypeErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeErrorAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeError'Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeError'_Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeError_Agda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeInCurrentAgda.Interaction.BasicOps
- typeInMetaAgda.Interaction.BasicOps
- typeInTypeAgda.Compiler.BackendAgda.TypeChecking.Monad.Options
- TypeKAgda.Compiler.MAlonzo.Misc
- TypeLevelReductionsAgda.Compiler.BackendAgda.TypeChecking.Monad.Base
- typeLevelReductionsAgda.Compiler.BackendAgda.TypeChecking.Monad.Env
- typeNameAgda.TypeChecking.Level
- TypeOfAgda.Syntax.Internal
- typeOfBVAgda.Compiler.BackendAgda.TypeChecking.Monad.Context
- typeOfConstAgda.Compiler.BackendAgda.TypeChecking.Monad.Signature
- typeOfFlatAgda.TypeChecking.Rules.Builtin.Coinduction
- typeOfInfAgda.TypeChecking.Rules.Builtin.Coinduction
- typeOfMetaAgda.Interaction.BasicOps
- typeOfMeta'Agda.Interaction.BasicOps
- typeOfMetaMIAgda.Interaction.BasicOps
- typeOfSharpAgda.TypeChecking.Rules.Builtin.Coinduction
- TypeSigAgda.BenchmarkingAgda.Syntax.ConcreteAgda.Utils.Haskell.Syntax
- typeSigAgda.Syntax.Parser.Helpers
- TypeSignatureAgda.Syntax.AbstractAgda.Syntax.Concrete
- TypeSignatureOrInstanceBlockAgda.Syntax.Concrete
- TypeSigsRHSAgda.Syntax.Parser.Helpers
- typesOfHiddenMetasAgda.Interaction.BasicOps
- typesOfVisibleMetasAgda.Interaction.BasicOps
- TypingAgda.Benchmarking
- TypstFileTypeAgda.Syntax.Common
- TyVarAgda.Utils.Haskell.Syntax
- TyVarBindAgda.Utils.Haskell.Syntax