Agda-2.8.0: 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.Mimer.Options
TACon | Agda.Syntax.Treeless, Agda.Compiler.Backend
Tactic | Agda.Syntax.Concrete
TacticAttribute |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Concrete
3 (Data Constructor) | Agda.Syntax.Concrete.Attribute
4 (Type/Class) | Agda.Syntax.Abstract
TacticAttribute' | Agda.Syntax.Concrete
TacticAttributeNotAllowed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TacticAttributeNotAllowed_ | Agda.Interaction.Options.Errors
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
tails1 | Agda.Utils.List1
tailWithDefault | Agda.Utils.List
take |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
takeAwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takeAwakeConstraint' | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
takeOptionsPragmas | Agda.Syntax.Parser.Helpers
takeP | Agda.Utils.Permutation
takeSizeConstraints | Agda.TypeChecking.SizedTypes
takeWhile | Agda.Utils.List1
takeWhileAntitone |
1 (Function) | Agda.Utils.Set1
2 (Function) | Agda.Utils.Map1
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 |
1 (Function) | Agda.Utils.BiMap
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional, Agda.Termination.CallGraph
TargetDef | Agda.Termination.Monad
targetNodes |
1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
2 (Function) | Agda.Termination.CallGraph
TargetOther | Agda.Termination.Monad
TargetRecord | Agda.Termination.Monad
tbFinite | Agda.Syntax.Abstract
TBind |
1 (Data Constructor) | Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Syntax.Abstract
tbTacticAttr | Agda.Syntax.Abstract
TCase | Agda.Syntax.Treeless, Agda.Compiler.Backend
TCEnv |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrClosErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrLocation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcErrString | Agda.TypeChecking.Errors
tcExec | Agda.TypeChecking.Unquote
TCM |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCMError | Agda.Interaction.ExitCode
TCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCoerce | Agda.Syntax.Treeless, Agda.Compiler.Backend
TCon | Agda.Syntax.Treeless, Agda.Compiler.Backend
TCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TCWarning |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningCached | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningDoc | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningLocation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningOrigin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Warnings, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tcWarningsToError | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors
tcWarningString | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.Internal
2 (Type/Class) | Agda.Syntax.Concrete
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
tell1 | Agda.Utils.Monad
tellDirty | Agda.Utils.Update
tellEmacsToJumpToError | Agda.Interaction.InteractionTop
tellEq | Agda.TypeChecking.Rewriting.NonLinMatch
tellSub | Agda.TypeChecking.Rewriting.NonLinMatch
tellToUpdateHighlighting | Agda.Interaction.InteractionTop
tellUnifyProof | Agda.TypeChecking.Rules.LHS.Unify.Types
tellUnifySubst | Agda.TypeChecking.Rules.LHS.Unify.Types
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
telViewPathBoundary | Agda.TypeChecking.Telescope
telViewUpTo | Agda.TypeChecking.Telescope
telViewUpTo' | Agda.TypeChecking.Telescope
telViewUpToPath | Agda.TypeChecking.Telescope
telViewUpToPathBoundary | Agda.TypeChecking.Telescope
telViewUpToPathBoundary' | Agda.TypeChecking.Telescope
TempInstanceTable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
TerEnv |
1 (Type/Class) | Agda.Termination.Monad
2 (Data Constructor) | Agda.Termination.Monad
terGetCurrent | Agda.Termination.Monad
terGetCutOff | 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.Syntax.Internal
2 (Type/Class) | Agda.Syntax.Reflected
terM | Agda.Termination.Monad
terMaskArgs | Agda.Termination.Monad
terMaskResult | Agda.Termination.Monad
termC | Agda.TypeChecking.Serialise.Base
termDecl | Agda.Termination.TermCheck
termErrCalls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
termErrFunctions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
termErrGuardednessHelps | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TermHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Terminates |
1 (Type/Class) | Agda.Termination.Termination
2 (Data Constructor) | Agda.Termination.Termination
terminates | Agda.Termination.Termination
terminatesFilter | Agda.Termination.Termination
TerminatesNot | 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.TypeChecking.Monad, Agda.Compiler.Backend
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TerminationIssue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TerminationIssue_ | Agda.Interaction.Options.Warnings
TerminationMeasure | Agda.Syntax.Common
TerminationProblem | Agda.Syntax.Common.Aspect, 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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TermSize | Agda.Syntax.Internal
termSize | Agda.Syntax.Internal
termsS | Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
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
terSetGuarded | Agda.Termination.Monad
terSetHaveInlinedWith | Agda.Termination.Monad
terSetMaskArgs | Agda.Termination.Monad
terSetMaskResult | Agda.Termination.Monad
terSetPatterns | Agda.Termination.Monad
TerSetSizeDepth | 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.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
textNonEmpty | Agda.Syntax.Common.Pretty
tgtNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional
thd3 | Agda.Utils.Tuple
theAttr | Agda.Syntax.Concrete.Attribute
theBlocker | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal
theBoundary | Agda.TypeChecking.Telescope
theCallGraph | Agda.Termination.CallGraph
theConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theCore | Agda.TypeChecking.Substitute
theCurrentFile | Agda.Interaction.Base
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theFileId | Agda.Utils.FileId
theFixity | Agda.Syntax.Common
TheFlexRigMap | Agda.TypeChecking.Free.Lazy
theFlexRigMap | Agda.TypeChecking.Free.Lazy
TheInfo | Agda.TypeChecking.Coverage.SplitClause
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.TypeChecking.Monad, Agda.Compiler.Backend
thenTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
theSize | Agda.Utils.Size
theSmallSet | Agda.Utils.SmallSet
theSolution | Agda.TypeChecking.SizedTypes.Syntax
theTacticAttribute | Agda.Syntax.Concrete
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
throwDecode | Agda.Interaction.JSON
throwDecode' | Agda.Interaction.JSON
throwDecodeStrict | Agda.Interaction.JSON
throwDecodeStrict' | Agda.Interaction.JSON
throwDecodeStrictText | Agda.Interaction.JSON
throwImpossible | Agda.Utils.Impossible
throwMultipleFixityDecls | Agda.Syntax.Concrete.Fixity
throwMultiplePolarityPragmas | Agda.Syntax.Concrete.Fixity
tick | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tickICode | Agda.TypeChecking.Serialise.Base
tickMax | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tickN | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tIfThenElse | Agda.Syntax.Treeless, Agda.Compiler.Backend
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
tLevelUniv | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
TLit | Agda.Syntax.Treeless, Agda.Compiler.Backend
tlmodOf | Agda.Compiler.MAlonzo.Misc
tMaybe | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
TmBoundary | Agda.TypeChecking.Telescope
tmBoundary | Agda.TypeChecking.Telescope
TMeta | Agda.Syntax.Treeless, Agda.Compiler.Backend
tmSort | Agda.Syntax.Internal
tmSSort | Agda.Syntax.Internal
tNegPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend
to | Agda.Interaction.Highlighting.Range
toAbsN | Agda.TypeChecking.Names
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.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.Bag
5 (Function) | Agda.Utils.BoolSet
6 (Function) | Agda.Utils.SmallSet
7 (Function) | Agda.Utils.Trie
toAtoms | Agda.Interaction.Highlighting.Common
toAttribute | Agda.Syntax.Parser.Helpers
toBool | Agda.Utils.Boolean
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete
toConcrete | Agda.Syntax.Translation.AbstractToConcrete
toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete
toConPatternInfo | Agda.Syntax.Internal
toCType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
toDescList |
1 (Function) | Agda.Utils.VarSet
2 (Function) | Agda.Utils.Set1
3 (Function) | Agda.Utils.Map1
toDistinctAscendingLists | Agda.Utils.BiMap
toEncoding | Agda.Interaction.JSON
toEncoding1 | Agda.Interaction.JSON
toEncoding2 | Agda.Interaction.JSON
toEncodingList | Agda.Interaction.JSON
toExpandLast | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
toFiniteList | Agda.Utils.IntSet.Infinite
toFinitePi | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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 |
1 (Type/Class) | Agda.Syntax.Parser.Tokens
2 (Type/Class) | Agda.Mimer.Options
token |
1 (Function) | Agda.Utils.Parser.MemoisedCPS
2 (Function) | Agda.Syntax.Parser.LexActions
TokenBased |
1 (Type/Class) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
tokenBased | Agda.Syntax.Common.Aspect, 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.List1, Agda.Utils.List2
2 (Function) | Agda.Utils.VarSet
3 (Function) | Agda.Utils.Map1
4 (Function) | Agda.Utils.Set1
5 (Function) | Agda.Utils.Bag
6 (Function) | Agda.Utils.HashTable
7 (Function) | Agda.Utils.BoolSet
8 (Function) | Agda.Utils.SmallSet
9 (Function) | Agda.Utils.Trie
10 (Function) | Agda.Utils.Favorites
11 (Function) | Agda.Utils.BiMap
12 (Function) | Agda.Termination.CallMatrix
13 (Function) | Agda.Termination.CallGraph
14 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
toList' | Agda.Utils.List1
toList1 | Agda.Utils.List2
toList1Either | Agda.Utils.List2
toListOrderedBy | Agda.Utils.Trie
toLists | Agda.Termination.SparseMatrix
toLType | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
toMap |
1 (Function) | Agda.Utils.Map1
2 (Function) | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise
toNamedArg | Agda.Syntax.Concrete
ToNLPat | Agda.TypeChecking.Rewriting.Clause
toNLPat | Agda.TypeChecking.Rewriting.Clause
TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooFewArgumentsToPatternSynonym_ | Agda.Interaction.Options.Errors
TooFewPatternsInWithClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooFewPatternsInWithClause_ | Agda.Interaction.Options.Errors
TooManyArgumentsToSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyArgumentsToSort_ | Agda.Interaction.Options.Warnings
TooManyFields |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Warning
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyFields_ |
1 (Data Constructor) | Agda.Interaction.Options.Warnings
2 (Data Constructor) | Agda.Interaction.Options.Errors
TooManyParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyParameters_ | Agda.Interaction.Options.Errors
TooManyPatternsInWithClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyPatternsInWithClause_ | Agda.Interaction.Options.Errors
TooManyPolarities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TooManyPolarities_ | Agda.Interaction.Options.Warnings
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
topLevelModuleFilePath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TopLevelModuleName |
1 (Data Constructor) | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
2 (Type/Class) | Agda.Syntax.TopLevelModuleName, Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
topLevelModuleName |
1 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Function) | Agda.Syntax.Translation.ConcreteToAbstract
3 (Function) | Agda.Compiler.Common
TopLevelModuleName' | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
TopLevelModuleNameParts | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName
topLevelModuleNameToQName | Agda.Syntax.TopLevelModuleName
TopLevelPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TopLevelPolarity_ | Agda.Interaction.Options.Warnings
topLevelScope | Agda.Syntax.Translation.ConcreteToAbstract
topLevelSourceFile | 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
topPolarity | Agda.Syntax.Common
topQuantity | Agda.Syntax.Common
topRelevance | Agda.Syntax.Common
topSort | Agda.Utils.Graph.TopSort
topVarOcc | Agda.TypeChecking.Free.Lazy
toReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
toSet | Agda.Utils.Set1
toSet' | Agda.Utils.Set1
toSingleton | Agda.Utils.BoolSet
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 |
1 (Function) | Agda.Utils.BoolSet
2 (Function) | Agda.Utils.SmallSet
ToTerm | Agda.TypeChecking.Primitive
toTerm | Agda.TypeChecking.Primitive
toTermTCM | Agda.TypeChecking.Primitive
toTree | Agda.TypeChecking.Coverage.SplitTree
toTreeless | Agda.Compiler.ToTreeless, Agda.Compiler.Backend
toTreelessWith | 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.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceCallCPS | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceCallCPS' | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceCallM | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceClosureCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceDebugMessage | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceM | Agda.TypeChecking.SizedTypes.Utils
TraceS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceS | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceSDoc | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
traceSLn | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
translateSplitTree | Agda.TypeChecking.RecordPatterns
TransparentDef | Agda.Syntax.Common
TranspError | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
TranspOp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpose |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional
3 (Function) | Agda.Termination.SparseMatrix
transposeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional
transpPathPTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpPathTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpSys | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpSysTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpTel | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
transpTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
traverse' | Agda.Utils.Bag
traverseAPatternM | Agda.Syntax.Abstract.Pattern
traverseArray_ | Agda.Utils.IArray
traverseCPatternA | Agda.Syntax.Concrete.Pattern
traverseCPatternM | Agda.Syntax.Concrete.Pattern
TraverseDecl | Agda.Syntax.Concrete.Generic
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
traverseMaybeWithKey | Agda.Utils.Map1
traverseMaybeWithKey1 | Agda.Utils.Map1
traversePatternM | Agda.Syntax.Internal.Pattern
traverseTermM | Agda.Syntax.Internal.Generic
traverseWithKey | Agda.Utils.Map1
traverseWithKey1 | Agda.Utils.Map1
TreeFileType | Agda.Syntax.Common
treelessPrimName | Agda.Compiler.MAlonzo.Primitives
trFillPathPTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillPathTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillTel | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
trFillTel' | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Trie |
1 (Type/Class) | Agda.Utils.Trie
2 (Data Constructor) | Agda.Utils.Trie
TriedToCopyConstrainedPrim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TriedToCopyConstrainedPrim_ | Agda.Interaction.Options.Errors
trim | Agda.Utils.String
trimLineComment | Agda.Interaction.Library.Parse
trivial | Agda.TypeChecking.SizedTypes
true | Agda.Utils.Boolean
trueCondition | Agda.TypeChecking.MetaVars
truncatedCallStack | Agda.Utils.CallStack
TruncateOffset | Agda.TypeChecking.SizedTypes.Syntax
truncateOffset | Agda.TypeChecking.SizedTypes.Syntax
tryAddBoundary | Agda.TypeChecking.MetaVars
tryCatch | Agda.Utils.Monad
tryConversion | Agda.TypeChecking.Conversion
tryConversion' | Agda.TypeChecking.Conversion
tryError | Agda.Utils.Monad
tryGetOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend
tryMaybe | Agda.Utils.Monad
tryRecordType | Agda.TypeChecking.Records
tryResolveName | Agda.Syntax.Scope.Monad
trySizeUniv | Agda.TypeChecking.SizedTypes
tryStrengthen | Agda.Compiler.Treeless.Subst
tryTranspError | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
tset | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
tsize | Agda.Syntax.Internal
tSizeUniv | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
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
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 (Type/Class) | Agda.Syntax.Internal
3 (Data Constructor) | Agda.Syntax.Internal
4 (Type/Class) | Agda.Syntax.Reflected
5 (Type/Class) | Agda.Syntax.Abstract
Type' | Agda.Syntax.Internal
Type'' | Agda.Syntax.Internal
typeAndFacesInMeta | Agda.Interaction.BasicOps
typeAnnotations | Agda.TypeChecking.Rules.LHS.Problem
typeArgsWithTel | Agda.TypeChecking.Substitute
typeArity | Agda.TypeChecking.Telescope
TypeCheck | Agda.Interaction.Imports
TypeCheckAction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeCheckMain | Agda.Interaction.Imports
TypeChecks | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
Typeclass | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
typeConArgsLeft | Agda.TypeChecking.Rules.LHS.Unify.Types
typeConArgsRight | Agda.TypeChecking.Rules.LHS.Unify.Types
typeConInjectAt | Agda.TypeChecking.Rules.LHS.Unify.Types
TypeConInjectivity | Agda.TypeChecking.Rules.LHS.Unify.Types
typeConstructor | Agda.TypeChecking.Rules.LHS.Unify.Types
TypedAssign | Agda.Interaction.Base
TypedBinding |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
TypedBinding' | Agda.Syntax.Concrete
TypedBindingInfo |
1 (Type/Class) | Agda.Syntax.Abstract
2 (Data Constructor) | Agda.Syntax.Abstract
TypeDecl | Agda.Utils.Haskell.Syntax
TypeDoesNotEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeElims | Agda.TypeChecking.Records
TypeError |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeError' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeError'_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeErrorName | Agda.TypeChecking.Errors.Names
typeErrorString | Agda.TypeChecking.Errors.Names
typeError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeInCurrent | Agda.Interaction.BasicOps
typeInMeta | Agda.Interaction.BasicOps
typeInType | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
TypeK | Agda.Compiler.MAlonzo.Misc
TypeLevelReductions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeLevelReductions | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeName | Agda.TypeChecking.Level
TypeOf | Agda.Syntax.Internal
typeOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
typeOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
typeSig | Agda.Syntax.Parser.Helpers
TypeSignature |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
TypeSignatureOrInstanceBlock | Agda.Syntax.Concrete
TypeSigsRHS | Agda.Syntax.Parser.Helpers
typesOfHiddenMetas | Agda.Interaction.BasicOps
typesOfVisibleMetas | Agda.Interaction.BasicOps
Typing | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
TypstFileType | Agda.Syntax.Common
TyVar | Agda.Utils.Haskell.Syntax
TyVarBind | Agda.Utils.Haskell.Syntax