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

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- -
- _
- All

Index - T

T | Agda.Auto.Options
TACon | Agda.Syntax.Treeless, Agda.Compiler.Backend
Tactic | Agda.Syntax.Concrete
TacticAttr | Agda.Syntax.Abstract
TacticAttribute |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete.Attribute
tacticAttributes | Agda.Syntax.Concrete.Attribute
Tag | Agda.Utils.BiMap
tag | Agda.Utils.BiMap
tagFieldName | Agda.Interaction.JSON
TaggedObject | Agda.Interaction.JSON
tagInjectiveFor | Agda.Utils.BiMap
tagSingleConstructors | Agda.Interaction.JSON
TAGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend
tail |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.List2
tailMaybe | Agda.Utils.List
tails | Agda.Utils.List1
tailWithDefault | Agda.Utils.List
take | Agda.Utils.List1
takeAwakeConstraint | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takeAwakeConstraint' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
takeP | Agda.Utils.Permutation
takeSizeConstraints | Agda.TypeChecking.SizedTypes
takeWhile | Agda.Utils.List1
takeWhileJust | Agda.Utils.List
TALit | Agda.Syntax.Treeless, Agda.Compiler.Backend
tallyDef | Agda.TypeChecking.MetaVars.Occurs
TAlt | Agda.Syntax.Treeless, Agda.Compiler.Backend
TApp | Agda.Syntax.Treeless, Agda.Compiler.Backend
tAppView | Agda.Syntax.Treeless, Agda.Compiler.Backend
Target | Agda.Termination.Monad
target | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
targetNodes |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function) | Agda.Termination.CallGraph
TBind |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
tcargs | Agda.Auto.Typecheck
TCase | Agda.Syntax.Treeless, Agda.Compiler.Backend
TCEnv |
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
TCErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrClosErr | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrLocation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcErrString | Agda.TypeChecking.Errors
tcExec | Agda.TypeChecking.Unquote
tcExp | Agda.Auto.Typecheck
TCM |
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
TCMError | Agda.Interaction.ExitCode
TCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCoerce | Agda.Syntax.Treeless, Agda.Compiler.Backend
TCon | Agda.Syntax.Treeless, Agda.Compiler.Backend
tcSearch | Agda.Auto.Typecheck
TCSt | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TCWarning |
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
tcWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningCached | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningLocation | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningOrigin | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningPrintedWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarningRange | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
tcWarnings | Agda.TypeChecking.Warnings
tcWarningsToError | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
TDef | Agda.Syntax.Treeless, Agda.Compiler.Backend
Tel |
1 (Type/Class) | Agda.Syntax.Concrete.Pretty
2 (Data Constructor) | Agda.Syntax.Concrete.Pretty
Tele | Agda.Syntax.Internal
tele2NamedArgs | Agda.TypeChecking.Telescope
teleArgNames | Agda.TypeChecking.Telescope
teleArgs | Agda.TypeChecking.Telescope
teleDoms | Agda.TypeChecking.Telescope
teleElims | Agda.TypeChecking.Telescope
teleLam | Agda.TypeChecking.Substitute
teleNamedArgs | Agda.TypeChecking.Telescope
teleNames | Agda.TypeChecking.Telescope
TeleNoAbs | Agda.TypeChecking.Substitute
teleNoAbs | Agda.TypeChecking.Substitute
telePatterns | Agda.TypeChecking.Telescope
telePatterns' | Agda.TypeChecking.Telescope
telePi | Agda.TypeChecking.Substitute
telePi' | Agda.TypeChecking.Substitute
telePiPath | Agda.TypeChecking.Telescope.Path
telePiPath_ | Agda.TypeChecking.Telescope.Path
telePiVisible | Agda.TypeChecking.Substitute
telePi_ | Agda.TypeChecking.Substitute
Telescope |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Internal
3 (Type/Class) | Agda.Syntax.Abstract
Telescope1 |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
telFromList | Agda.Syntax.Internal
telFromList' | Agda.Syntax.Internal
tellDirty | Agda.Utils.Update
tellEmacsToJumpToError | Agda.Interaction.InteractionTop
tellEq | Agda.TypeChecking.Rewriting.NonLinMatch
tellSub | Agda.TypeChecking.Rewriting.NonLinMatch
tellToUpdateHighlighting | Agda.Interaction.InteractionTop
TelToArgs | Agda.Syntax.Internal
telToArgs | Agda.Syntax.Internal
telToList | Agda.Syntax.Internal
TelV |
1 (Type/Class) | Agda.TypeChecking.Substitute
2 (Data Constructor) | Agda.TypeChecking.Substitute
telVars | Agda.TypeChecking.Substitute
TelView | Agda.TypeChecking.Substitute
telView | Agda.TypeChecking.Telescope
telView' | Agda.TypeChecking.Substitute
telView'Path | Agda.TypeChecking.Telescope
telView'UpTo | Agda.TypeChecking.Substitute
telView'UpToPath | Agda.TypeChecking.Telescope
telViewPath | Agda.TypeChecking.Telescope
telViewPathBoundaryP | Agda.TypeChecking.Telescope
telViewUpTo | Agda.TypeChecking.Telescope
telViewUpTo' | Agda.TypeChecking.Telescope
telViewUpToPath | Agda.TypeChecking.Telescope
telViewUpToPathBoundary | Agda.TypeChecking.Telescope
telViewUpToPathBoundary' | Agda.TypeChecking.Telescope
telViewUpToPathBoundaryP | Agda.TypeChecking.Telescope
TempInstanceTable | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Tentative | Agda.Syntax.Parser.Monad
TErased | Agda.Syntax.Treeless, Agda.Compiler.Backend
terAsk | Agda.Termination.Monad
terAsks | Agda.Termination.Monad
terCurrent | Agda.Termination.Monad
terCutOff | Agda.Termination.Monad
terDelayed | Agda.Termination.Monad
TerEnv |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
terGetCurrent | Agda.Termination.Monad
terGetCutOff | Agda.Termination.Monad
terGetDelayed | Agda.Termination.Monad
terGetGuarded | Agda.Termination.Monad
terGetHaveInlinedWith | Agda.Termination.Monad
terGetMaskArgs | Agda.Termination.Monad
terGetMaskResult | Agda.Termination.Monad
terGetMutual | Agda.Termination.Monad
terGetPatterns | Agda.Termination.Monad
terGetSharp | Agda.Termination.Monad
terGetSizeSuc | Agda.Termination.Monad
terGetTarget | Agda.Termination.Monad
terGetUsableVars | Agda.Termination.Monad
terGetUseDotPatterns | Agda.Termination.Monad
terGetUserNames | Agda.Termination.Monad
terGetUseSizeLt | Agda.Termination.Monad
terGuarded | Agda.Termination.Monad
terHaveInlinedWith | Agda.Termination.Monad
terLocal | Agda.Termination.Monad
TerM |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
Term |
1 (Type/Class) | Agda.Auto.NarrowingSearch
2 (Data Constructor) | Agda.Auto.NarrowingSearch
3 (Type/Class) | Agda.Syntax.Internal
4 (Type/Class) | Agda.Syntax.Reflected
terM | Agda.Termination.Monad
term | Agda.Compiler.MAlonzo.Compiler
terMaskArgs | Agda.Termination.Monad
terMaskResult | Agda.Termination.Monad
termC | Agda.TypeChecking.Serialise.Base
termD | Agda.TypeChecking.Serialise.Base
termDecl | Agda.Termination.TermCheck
termErrCalls | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
termErrFunctions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TermHead | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
terminates | Agda.Termination.Termination
terminatesFilter | Agda.Termination.Termination
Terminating | Agda.Syntax.Common
Termination | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TerminationCheck |
1 (Type/Class) | Agda.Syntax.Common
2 (Data Constructor) | Agda.Syntax.Common
3 (Type/Class) | Agda.Syntax.Concrete.Definitions.Types
terminationCheck | Agda.Syntax.Concrete.Definitions.Types
TerminationCheckPragma | Agda.Syntax.Concrete
terminationCheckPragma | Agda.Syntax.Concrete.Definitions.Monad
TerminationError |
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
TerminationIssue | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TerminationIssue_ | Agda.Interaction.Options.Warnings
TerminationMeasure | Agda.Syntax.Common
TerminationProblem | Agda.Interaction.Highlighting.Precise
TermLike | Agda.Syntax.Internal.Generic
termMutual | Agda.Termination.TermCheck
terModifyGuarded | Agda.Termination.Monad
terModifyUsableVars | Agda.Termination.Monad
terModifyUseSizeLt | Agda.Termination.Monad
TermPart | Agda.TypeChecking.Unquote
TermPosition | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
TermSize | Agda.Syntax.Internal
termSize | Agda.Syntax.Internal
TermSubst | Agda.TypeChecking.Substitute.Class, Agda.TypeChecking.Substitute
TermToPattern | Agda.TypeChecking.Patterns.Internal
termToPattern | Agda.TypeChecking.Patterns.Internal
terMutual | Agda.Termination.Monad
terPatterns | Agda.Termination.Monad
terPatternsRaise | Agda.Termination.Monad
terRaise | Agda.Termination.Monad
TError |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
terSetCurrent | Agda.Termination.Monad
terSetDelayed | Agda.Termination.Monad
terSetGuarded | Agda.Termination.Monad
terSetHaveInlinedWith | Agda.Termination.Monad
terSetMaskArgs | Agda.Termination.Monad
terSetMaskResult | Agda.Termination.Monad
terSetPatterns | Agda.Termination.Monad
terSetSizeDepth | Agda.Termination.Monad
terSetTarget | Agda.Termination.Monad
terSetUsableVars | Agda.Termination.Monad
terSetUseDotPatterns | Agda.Termination.Monad
terSetUseSizeLt | Agda.Termination.Monad
terSharp | Agda.Termination.Monad
terSizeDepth | Agda.Termination.Monad
terSizeSuc | Agda.Termination.Monad
terTarget | Agda.Termination.Monad
terUnguarded | Agda.Termination.Monad
terUsableVars | Agda.Termination.Monad
terUseDotPatterns | Agda.Termination.Monad
terUserNames | Agda.Termination.Monad
terUseSizeLt | Agda.Termination.Monad
testLub | Agda.TypeChecking.SizedTypes.WarshallSolver
testSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver
TexFileType | Agda.Syntax.Common
text |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
tgtNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
thd3 | Agda.Utils.Tuple
theBenchmark | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theBlocker | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
theCallGraph | Agda.Termination.CallGraph
theConstraint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theCore | Agda.TypeChecking.Substitute
theCurrentFile | Agda.Interaction.Base
theDef | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theDefLens | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theEtaEquality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theFixity | Agda.Syntax.Common
TheFlexRigMap | Agda.TypeChecking.Free.Lazy
theFlexRigMap | Agda.TypeChecking.Free.Lazy
theInteractionPoints | Agda.Interaction.Base
theKind | Agda.Syntax.Scope.Base
theMetaSet | Agda.TypeChecking.Free.Lazy
theNameRange | Agda.Syntax.Common
theNotation | Agda.Syntax.Common
thenReduce | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
thenTCMT | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
theSize | Agda.Utils.Size
theSolution | Agda.TypeChecking.SizedTypes.Syntax
theTel | Agda.TypeChecking.Substitute
TheVarMap | Agda.TypeChecking.Free.Lazy
theVarMap | Agda.TypeChecking.Free.Lazy
TheVarMap' | Agda.TypeChecking.Free.Lazy
ThingsInScope | Agda.Syntax.Scope.Base
thingsInScope | Agda.Syntax.Scope.Base
ThingWithFixity |
1 (Type/Class) | Agda.Syntax.Fixity, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Fixity, Agda.Syntax.Concrete
Three |
1 (Type/Class) | Agda.Utils.Three
2 (Data Constructor) | Agda.Utils.Three
throwImpossible | Agda.Utils.Impossible
throwMultipleFixityDecls | Agda.Syntax.Concrete.Fixity
throwMultiplePolarityPragmas | Agda.Syntax.Concrete.Fixity
tick | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
tickICode | Agda.TypeChecking.Serialise.Base
tickMax | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
tickN | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics
tIfThenElse | Agda.Syntax.Treeless, Agda.Compiler.Backend
TimeOut |
1 (Type/Class) | Agda.Auto.Options
2 (Data Constructor) | Agda.Auto.Options
Timings | Agda.Utils.Benchmark
timings | Agda.Utils.Benchmark
tInt | Agda.Syntax.Treeless, Agda.Compiler.Backend
TLam | Agda.Syntax.Treeless, Agda.Compiler.Backend
tLamView | Agda.Syntax.Treeless, Agda.Compiler.Backend
TLet |
1 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Abstract
tLetView | Agda.Syntax.Treeless, Agda.Compiler.Backend
TLit | Agda.Syntax.Treeless, Agda.Compiler.Backend
tlmodOf | Agda.Compiler.MAlonzo.Misc
TMAll | Agda.Auto.Convert
tMaybe | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
TMeta | Agda.Syntax.Treeless, Agda.Compiler.Backend
TMode | Agda.Auto.Convert
tmSort | Agda.Syntax.Internal
tmSSort | Agda.Syntax.Internal
tNegPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend
to | Agda.Interaction.Highlighting.Range
toAbsName | Agda.TypeChecking.Serialise.Instances.Abstract
ToAbstract |
1 (Type/Class) | Agda.Syntax.Translation.ReflectedToAbstract
2 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract
toAbstract |
1 (Function) | Agda.Syntax.Translation.ReflectedToAbstract
2 (Function) | Agda.Syntax.Translation.ConcreteToAbstract
toAbstractWithoutImplicit | Agda.Syntax.Translation.ReflectedToAbstract
toAbstract_ | Agda.Syntax.Translation.ReflectedToAbstract
ToArgs | Agda.Interaction.JSON
toAscList |
1 (Function) | Agda.Utils.Bag
2 (Function) | Agda.Utils.SmallSet
3 (Function) | Agda.Utils.Trie
toAtoms | Agda.Interaction.Highlighting.Common
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete
toConcrete | Agda.Syntax.Translation.AbstractToConcrete
toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete
toConPatternInfo | Agda.Syntax.Internal
toCType | Agda.TypeChecking.Rules.Data
toDescList | Agda.Utils.VarSet
toDistinctAscendingLists | Agda.Utils.BiMap
toEncoding | Agda.Interaction.JSON
toEncoding1 | Agda.Interaction.JSON
toEncoding2 | Agda.Interaction.JSON
toEncodingList | Agda.Interaction.JSON
toFiniteList | Agda.Utils.IntSet.Infinite
ToggleImplicitArgs | Agda.Interaction.Base
ToggleIrrelevantArgs | Agda.Interaction.Base
toIFile | Agda.Interaction.FindFile
toImpossible | Agda.Utils.Empty
ToJSON | Agda.Interaction.JSON
toJSON | Agda.Interaction.JSON
ToJSON1 | Agda.Interaction.JSON
toJSON1 | Agda.Interaction.JSON
ToJSON2 | Agda.Interaction.JSON
toJSON2 | Agda.Interaction.JSON
ToJSONKey | Agda.Interaction.JSON
toJSONKey | Agda.Interaction.JSON
ToJSONKeyFunction | Agda.Interaction.JSON
toJSONKeyList | Agda.Interaction.JSON
ToJSONKeyText | Agda.Interaction.JSON
ToJSONKeyValue | Agda.Interaction.JSON
toJSONList | Agda.Interaction.JSON
tok | Agda.Utils.Parser.MemoisedCPS
TokComment | Agda.Syntax.Parser.Tokens
TokDummy | Agda.Syntax.Parser.Tokens
Token | Agda.Syntax.Parser.Tokens
token |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Parser.LexActions
TokenBased |
1 (Type/Class) | Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
tokenBased | Agda.Interaction.Highlighting.Precise
TokenLength | Agda.Syntax.Parser.Alex
tokensParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
TokEOF | Agda.Syntax.Parser.Tokens
TokId | Agda.Syntax.Parser.Tokens
TokKeyword | Agda.Syntax.Parser.Tokens
TokLiteral | Agda.Syntax.Parser.Tokens
TokMarkup | Agda.Syntax.Parser.Tokens
TokQId | Agda.Syntax.Parser.Tokens
TokString | Agda.Syntax.Parser.Tokens
TokSymbol | Agda.Syntax.Parser.Tokens
TokTeX | Agda.Syntax.Parser.Tokens
toLazy | Agda.Utils.Maybe.Strict
toList |
1 (Function) | Agda.Utils.List2
2 (Function) | Agda.Utils.List1
3 (Function) | Agda.Utils.VarSet
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.SmallSet
6 (Function) | Agda.Utils.Trie
7 (Function) | Agda.Utils.BiMap
8 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
9 (Function) | Agda.Utils.Favorites
10 (Function) | Agda.Termination.CallMatrix
11 (Function) | Agda.Termination.CallGraph
toList1 | Agda.Utils.List2
toListOrderedBy | Agda.Utils.Trie
toLists | Agda.Termination.SparseMatrix
toLType | Agda.TypeChecking.Rules.Data
TOM | Agda.Auto.Convert
toMap | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
tomy | Agda.Auto.Convert
tomyIneq | Agda.Auto.Convert
ToNLPat | Agda.TypeChecking.Rewriting.Clause
toNLPat | Agda.TypeChecking.Rewriting.Clause
TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFields | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFieldsWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TooManyFieldsWarning_ | Agda.Interaction.Options.Warnings
TooManyPolarities | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
toOrderings | Agda.Utils.PartialOrd
Top | Agda.TypeChecking.SizedTypes.Utils
tOp | Agda.Syntax.Treeless, Agda.Compiler.Backend
top | Agda.TypeChecking.SizedTypes.Utils
topBlock | Agda.Syntax.Parser.Monad
topCohesion | Agda.Syntax.Common
TopCtx | Agda.Syntax.Fixity
TopK | Agda.Syntax.Concrete.Operators.Parser.Monad
TopLevel |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract
topLevelArg | Agda.TypeChecking.Injectivity
topLevelDecls | Agda.Syntax.Translation.ConcreteToAbstract
topLevelExpectedName | Agda.Syntax.Translation.ConcreteToAbstract
TopLevelInfo |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract
topLevelModuleDropper | Agda.TypeChecking.Errors
TopLevelModuleName |
1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
topLevelModuleName |
1 (Function) | Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Translation.ConcreteToAbstract
3 (Function) | Agda.Compiler.Common
topLevelPath | Agda.Syntax.Translation.ConcreteToAbstract
topLevelScope | Agda.Syntax.Translation.ConcreteToAbstract
topLevelTheThing | Agda.Syntax.Translation.ConcreteToAbstract
topModality | Agda.Syntax.Common
TopModule | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TopOpenModule | Agda.Syntax.Scope.Monad
topoSort | Agda.Utils.Permutation
topoSortM | Agda.Utils.Permutation
topQuantity | Agda.Syntax.Common
topRelevance | Agda.Syntax.Common
topSearch | Agda.Auto.NarrowingSearch
topSort | Agda.Utils.Graph.TopSort
topVarOcc | Agda.TypeChecking.Free.Lazy
toSparseRows | Agda.Termination.SparseMatrix
toSplitPatterns | Agda.TypeChecking.Coverage.Match
toSplitPSubst | Agda.TypeChecking.Coverage.Match
toStrict | Agda.Utils.Maybe.Strict
toStringWithoutDotZero | Agda.Utils.Float
toSubscriptDigit | Agda.Utils.Suffix
total | Agda.Utils.SmallSet
ToTerm | Agda.TypeChecking.Primitive
toTerm | Agda.TypeChecking.Primitive
toTermR | Agda.TypeChecking.Primitive
toTopLevelModuleName |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
toTree | Agda.TypeChecking.Coverage.SplitTree
toTreeless | Agda.Compiler.Backend, Agda.Compiler.ToTreeless
toTrees | Agda.TypeChecking.Coverage.SplitTree
toVim | Agda.Interaction.Highlighting.Vim
toWeight | Agda.TypeChecking.SizedTypes.WarshallSolver
TPFn | Agda.Syntax.Treeless, Agda.Compiler.Backend
tPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend
TPOp | Agda.Syntax.Treeless, Agda.Compiler.Backend
TPrim |
1 (Type/Class) | Agda.Syntax.Treeless, Agda.Compiler.Backend
2 (Data Constructor) | Agda.Syntax.Treeless, Agda.Compiler.Backend
trace | Agda.TypeChecking.SizedTypes.Utils
traceCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceCallCPS | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceCallM | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceClosureCall | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace
traceDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceM | Agda.TypeChecking.SizedTypes.Utils
TraceS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceS | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceSDoc | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
traceSLn | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
trailingWithPatterns | Agda.Syntax.Abstract.Pattern
trampoline | Agda.Utils.Function
trampolineM | Agda.Utils.Function
trampolineWhile | Agda.Utils.Function
trampolineWhileM | Agda.Utils.Function
transClos | Agda.TypeChecking.SizedTypes.WarshallSolver
transform | Agda.Compiler.Treeless.EliminateLiteralPatterns
transitiveClosure | Agda.Utils.Graph.AdjacencyMap.Unidirectional
transitiveReduction | Agda.Utils.Graph.AdjacencyMap.Unidirectional
translateBuiltins | Agda.Compiler.Treeless.Builtin
translateCompiledClauses | Agda.TypeChecking.RecordPatterns
translateRecordPatterns | Agda.TypeChecking.RecordPatterns
translateSplitTree | Agda.TypeChecking.RecordPatterns
TranspOrHComp | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
transpose |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function) | Agda.Termination.SparseMatrix
transposeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
transpTel | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
Trav | Agda.Auto.NarrowingSearch
trav | Agda.Auto.NarrowingSearch
traverse' | Agda.Utils.Bag
traverseAPatternM | Agda.Syntax.Abstract.Pattern
traverseCPatternA | Agda.Syntax.Concrete.Pattern
traverseCPatternM | Agda.Syntax.Concrete.Pattern
traverseEither | Agda.Utils.Either
traverseExpr |
1 (Function) | Agda.Syntax.Concrete.Generic
2 (Function) | Agda.Syntax.Abstract.Views
TraverseExprFn | Agda.Syntax.Abstract.Views
TraverseExprRecFn | Agda.Syntax.Abstract.Views
traverseF | Agda.Utils.Functor
traversePatternM | Agda.Syntax.Internal.Pattern
traversePi | Agda.Auto.Typecheck
traverseTermM | Agda.Syntax.Internal.Generic
TravWith | Agda.Auto.NarrowingSearch
TrBr |
1 (Type/Class) | Agda.Auto.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
treatAbstractly | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
treatAbstractly' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
treelessPrimName | Agda.Compiler.MAlonzo.Primitives
trFillTel | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
Trie |
1 (Type/Class) | Agda.Utils.Trie
2 (Data Constructor) | Agda.Utils.Trie
TriedToCopyConstrainedPrim | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
trim | Agda.Utils.String
trimLineComment | Agda.Interaction.Library.Parse
trivial | Agda.TypeChecking.SizedTypes
trueCondition | Agda.TypeChecking.MetaVars
truncatedCallStack | Agda.Utils.CallStack
TruncateOffset | Agda.TypeChecking.SizedTypes.Syntax
truncateOffset | Agda.TypeChecking.SizedTypes.Syntax
tryCatch | Agda.Utils.Monad
tryConversion | Agda.TypeChecking.Conversion
tryConversion' | Agda.TypeChecking.Conversion
tryGetOpen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open
tryMaybe | Agda.Utils.Monad
tryRecordType | Agda.TypeChecking.Records
tryResolveName | Agda.Syntax.Scope.Monad
trySizeUniv | Agda.TypeChecking.SizedTypes
tryStrengthen | Agda.Compiler.Treeless.Subst
tset | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
tsize | Agda.Syntax.Internal
tSizeUniv | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
TSort | Agda.Syntax.Treeless, Agda.Compiler.Backend
TTerm | Agda.Syntax.Treeless, Agda.Compiler.Backend
TUnit | Agda.Syntax.Treeless, Agda.Compiler.Backend
TUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend
tUnreachable | Agda.Syntax.Treeless, Agda.Compiler.Backend
tvaldecl | Agda.Compiler.MAlonzo.Compiler
TVar | Agda.Syntax.Treeless, Agda.Compiler.Backend
Two | Agda.Utils.Three
TwoElemArray | Agda.Interaction.JSON
TyApp | Agda.Utils.Haskell.Syntax
TyCon | Agda.Utils.Haskell.Syntax
TyForall | Agda.Utils.Haskell.Syntax
TyFun | Agda.Utils.Haskell.Syntax
Type |
1 (Type/Class) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Auto.Syntax
3 (Data Constructor) | Agda.Syntax.Internal
4 (Type/Class) | Agda.Syntax.Internal
5 (Type/Class) | Agda.Syntax.Reflected
Type' | Agda.Syntax.Internal
Type'' | Agda.Syntax.Internal
typeAnnotations | Agda.TypeChecking.Rules.LHS.Problem
typeArgsWithTel | Agda.TypeChecking.Substitute
typeArity | Agda.TypeChecking.Telescope
TypeCheck | Agda.Interaction.Imports
TypeCheckAction | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeCheckMain | Agda.Interaction.Imports
TypeChecks | Agda.Interaction.Highlighting.Precise
TypedAssign | Agda.Interaction.Base
TypedBinding |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
TypedBinding' | Agda.Syntax.Concrete
TypeDecl | Agda.Utils.Haskell.Syntax
typeElims | Agda.TypeChecking.Records
TypeError |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError' | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError'_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeError_ | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeInCurrent | Agda.Interaction.BasicOps
typeInMeta | Agda.Interaction.BasicOps
typeInType | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
TypeK | Agda.Compiler.MAlonzo.Misc
TypeLevelReductions | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
typeLevelReductions | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env
typeName | Agda.TypeChecking.Level
typeOfBV | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context
typeOfConst | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
typeOfFlat | Agda.TypeChecking.Rules.Builtin.Coinduction
typeOfInf | Agda.TypeChecking.Rules.Builtin.Coinduction
typeOfMeta | Agda.Interaction.BasicOps
typeOfMeta' | Agda.Interaction.BasicOps
typeOfMetaMI | Agda.Interaction.BasicOps
typeOfSharp | Agda.TypeChecking.Rules.Builtin.Coinduction
TypeSig |
1 (Data Constructor) | Agda.Utils.Haskell.Syntax
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TypeSignature |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
TypeSignatureOrInstanceBlock | Agda.Syntax.Concrete
typesOfHiddenMetas | Agda.Interaction.BasicOps
typesOfVisibleMetas | Agda.Interaction.BasicOps
Typing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TyVar | Agda.Utils.Haskell.Syntax
TyVarBind | Agda.Utils.Haskell.Syntax