T | Agda.Auto.Options |
TACon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Tactic | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
TAGuard | Agda.Syntax.Treeless, Agda.Compiler.Backend |
takeAwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
takeI | Agda.Syntax.Position |
takeP | Agda.Utils.Permutation |
takeRelevant | Agda.TypeChecking.MetaVars.Occurs |
takeSizeConstraints | Agda.TypeChecking.SizedTypes |
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.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 |
tcErrState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
tcErrString | Agda.TypeChecking.Errors |
tcExp | Agda.Auto.Typecheck |
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 |
TCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TCon | Agda.Syntax.Treeless, Agda.Compiler.Backend |
tcSearch | Agda.Auto.Typecheck |
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 |
tcWarningOrigin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
tcWarningPrintedWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
tcWarningRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
tcWarningsToError | 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 |
TelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Tele | Agda.Syntax.Internal |
tele2NamedArgs | Agda.TypeChecking.Telescope |
teleArgNames | Agda.TypeChecking.Telescope |
teleArgs | Agda.TypeChecking.Telescope |
teleLam | Agda.TypeChecking.Substitute |
teleNamedArgs | Agda.TypeChecking.Telescope |
teleNames | Agda.TypeChecking.Telescope |
TeleNoAbs | Agda.TypeChecking.Substitute |
teleNoAbs | Agda.TypeChecking.Substitute |
telePi | Agda.TypeChecking.Substitute |
telePi' | 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 |
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'UpTo | Agda.TypeChecking.Substitute |
telViewUpTo | Agda.TypeChecking.Telescope |
telViewUpTo' | Agda.TypeChecking.Telescope |
TempInstanceTable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
terGetGuardingTypeConstructors | Agda.Termination.Monad |
terGetHaveInlinedWith | Agda.Termination.Monad |
terGetInlineWithFunctions | 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 |
terGuardingTypeConstructors | Agda.Termination.Monad |
terHaveInlinedWith | Agda.Termination.Monad |
terInlineWithFunctions | 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.Reflected |
4 (Type/Class) | Agda.Syntax.Internal |
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.TypeChecking.Monad, Agda.Compiler.Backend |
termErrFunctions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TermHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
TerminationCheckFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TerminationCheckPragma | Agda.Syntax.Concrete |
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 |
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 |
TermSize | Agda.Syntax.Internal |
termSize | Agda.Syntax.Internal |
terMutual | Agda.Termination.Monad |
terPatterns | Agda.Termination.Monad |
terPatternsRaise | Agda.Termination.Monad |
terPiGuarded | 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 |
testChar | Agda.Utils.Char |
testLub | Agda.TypeChecking.SizedTypes.WarshallSolver |
testSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
text | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
tgtNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
thd3 | Agda.Utils.Tuple |
theBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theBlockingMeta | Agda.Syntax.Internal |
theCallGraph | Agda.Termination.CallGraph |
theConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theCore | Agda.TypeChecking.Substitute |
theCurrentFile | Agda.Interaction.InteractionTop |
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theDefLens | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theFixity | Agda.Syntax.Fixity |
theInteractionPoints | Agda.Interaction.InteractionTop |
theNameRange | Agda.Syntax.Fixity |
theNotation | Agda.Syntax.Fixity |
thenTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theSize | Agda.Utils.Size |
theSolution | Agda.TypeChecking.SizedTypes.Syntax |
theTel | Agda.TypeChecking.Substitute |
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 |
throwError | Agda.Utils.Except |
throwImpossible | Agda.Utils.Impossible |
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 |
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 |
TMode | Agda.Auto.Convert |
tNegPlusK | Agda.Syntax.Treeless, Agda.Compiler.Backend |
to | Agda.Interaction.Highlighting.Range |
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 |
toAbstractPats | Agda.Syntax.Translation.ReflectedToAbstract |
toAbstractWithoutImplicit | Agda.Syntax.Translation.ReflectedToAbstract |
toAbstract_ | Agda.Syntax.Translation.ReflectedToAbstract |
toAscList | |
1 (Function) | Agda.Utils.Bag |
2 (Function) | Agda.Utils.Trie |
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete |
toConcrete | Agda.Syntax.Translation.AbstractToConcrete |
toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
toConPatternInfo | Agda.Syntax.Internal |
toDescList | Agda.Utils.VarSet |
ToggleImplicitArgs | Agda.Interaction.InteractionTop |
toIFile | Agda.Interaction.FindFile |
toImpossible | Agda.Utils.Empty |
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 |
TokenLength | Agda.Syntax.Parser.Alex |
tokensParser | |
1 (Function) | Agda.Syntax.Parser.Parser |
2 (Function) | Agda.Syntax.Parser |
tokenStream | Agda.Interaction.Highlighting.HTML |
TokEOF | Agda.Syntax.Parser.Tokens |
TokId | Agda.Syntax.Parser.Tokens |
TokKeyword | Agda.Syntax.Parser.Tokens |
TokLiteral | Agda.Syntax.Parser.Tokens |
TokQId | Agda.Syntax.Parser.Tokens |
TokSetN | 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.VarSet |
2 (Function) | Agda.Utils.BiMap |
3 (Function) | Agda.Utils.HashMap |
4 (Function) | Agda.Utils.Bag |
5 (Function) | Agda.Utils.Trie |
6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
7 (Function) | Agda.Utils.Favorites |
8 (Function) | Agda.Termination.CallMatrix |
9 (Function) | Agda.Termination.CallGraph |
toListOrderedBy | Agda.Utils.Trie |
toLists | Agda.Termination.SparseMatrix |
TOM | Agda.Auto.Convert |
toMap | Agda.Interaction.Highlighting.Precise |
tomy | Agda.Auto.Convert |
tomyIneq | Agda.Auto.Convert |
TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooFewFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyArgumentsInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyPolarities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
toOrderings | Agda.Utils.PartialOrd |
Top | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
tOp | Agda.Syntax.Treeless, Agda.Compiler.Backend |
top | Agda.TypeChecking.SizedTypes.Utils |
topContext | Agda.Syntax.Parser.Monad |
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 |
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 |
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 |
TopModule | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
topoSort | Agda.Utils.Permutation |
topSearch | Agda.Auto.NarrowingSearch |
topSort | Agda.Syntax.Internal |
topVarOcc | Agda.TypeChecking.Free.Lazy |
toSparseRows | Agda.Termination.SparseMatrix |
toStrict | Agda.Utils.Maybe.Strict |
toSubscriptDigit | Agda.Utils.Suffix |
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.ToTreeless, Agda.Compiler.Backend |
toTrees | Agda.TypeChecking.Coverage.SplitTree |
toVim | Agda.Interaction.Highlighting.Vim |
toWeight | Agda.TypeChecking.SizedTypes.WarshallSolver |
tPlusK | 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 |
traceCallE | Agda.TypeChecking.Rules.Term |
traceCallM | 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 |
traceSDoc | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
traceSLn | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
translateBuiltins | Agda.Compiler.Treeless.Builtin |
translateCompiledClauses | Agda.TypeChecking.RecordPatterns |
translateCopatternClauses | Agda.Syntax.Abstract.Copatterns |
translateRecordPatterns | Agda.TypeChecking.RecordPatterns |
translateSplitTree | Agda.TypeChecking.RecordPatterns |
transpose | Agda.Termination.SparseMatrix |
transposeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Trav | Agda.Auto.NarrowingSearch |
trav | Agda.Auto.NarrowingSearch |
traverse' | Agda.Utils.Bag |
traverseAPatternM | Agda.Syntax.Abstract.Pattern |
traverseEither | Agda.Utils.Either |
traverseExpr | |
1 (Function) | Agda.Syntax.Concrete.Generic |
2 (Function) | Agda.Syntax.Abstract.Views |
traverseF | Agda.Utils.Functor |
traversePatternM | Agda.Syntax.Internal.Pattern |
traversePi | Agda.Auto.Typecheck |
traverseTermM | Agda.Syntax.Internal.Generic |
traverseWithKey | Agda.Utils.HashMap |
TrBr | |
1 (Type/Class) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Auto.Syntax |
treatAbstractly | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
treatAbstractly' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
treelessPrimName | Agda.Compiler.MAlonzo.Primitives |
Trie | |
1 (Type/Class) | Agda.Utils.Trie |
2 (Data Constructor) | Agda.Utils.Trie |
trim | Agda.Utils.String |
trimLineComment | Agda.Interaction.Library.Parse |
trivial | Agda.TypeChecking.SizedTypes |
trueCondition | Agda.TypeChecking.MetaVars |
TruncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
truncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
tryConversion | Agda.TypeChecking.Conversion |
tryConversion' | Agda.TypeChecking.Conversion |
tryMaybe | Agda.Utils.Monad |
tryOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
tryRecordType | Agda.TypeChecking.Records |
trySizeUniv | Agda.TypeChecking.SizedTypes |
tset | Agda.TypeChecking.Primitive |
tSetOmega | Agda.TypeChecking.Primitive |
tsize | Agda.Syntax.Internal |
tSizeUniv | 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 |
TurnIntoErrors | Agda.Interaction.Options |
tvaldecl | Agda.Compiler.MAlonzo.Compiler |
TVar | Agda.Syntax.Treeless, Agda.Compiler.Backend |
Two | Agda.Utils.Three |
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 (Type/Class) | Agda.Syntax.Reflected |
4 (Data Constructor) | Agda.Syntax.Internal |
5 (Type/Class) | Agda.Syntax.Internal |
Type' | Agda.Syntax.Internal |
typeArgsWithTel | Agda.TypeChecking.Substitute |
typeArity | Agda.TypeChecking.Telescope |
TypeCheck | Agda.Interaction.Imports |
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.Interaction.Highlighting.Precise |
TypeCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TypedAssign | Agda.Interaction.BasicOps |
TypedBinding | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
TypedBinding' | Agda.Syntax.Concrete |
TypedBindings | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Abstract |
TypedBindings' | Agda.Syntax.Concrete |
TypeDecl | Agda.Utils.Haskell.Syntax |
typeDontCare | Agda.Syntax.Internal |
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 |
typeIn | Agda.Interaction.CommandLine |
typeInCurrent | Agda.Interaction.BasicOps |
typeInMeta | Agda.Interaction.BasicOps |
typeInType | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
typeName | Agda.TypeChecking.Level |
typeOf | |
1 (Function) | Agda.TypeChecking.Abstract |
2 (Function) | Agda.Interaction.CommandLine |
typeOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |