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 |
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 | Agda.Utils.List1 |
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 |
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 |
tcWarningLocation | 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 |
tcWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Warnings, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |
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.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 |
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 |
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 |
tgtNodes | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
thd3 | Agda.Utils.Tuple |
theAttr | Agda.Syntax.Parser.Helpers |
theBenchmark | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theBlocker | Agda.Syntax.Internal.Blockers, 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.Base |
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
theEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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.BoolSet |
2 (Function) | Agda.Utils.Bag |
3 (Function) | Agda.Utils.SmallSet |
4 (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 | Agda.Utils.VarSet |
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.HashTable |
4 (Function) | Agda.Utils.BoolSet |
5 (Function) | Agda.Utils.Bag |
6 (Function) | Agda.Utils.SmallSet |
7 (Function) | Agda.Utils.Trie |
8 (Function) | Agda.Utils.Favorites |
9 (Function) | Agda.Utils.BiMap |
10 (Function) | Agda.Termination.CallMatrix |
11 (Function) | Agda.Termination.CallGraph |
12 (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 | Agda.Utils.RangeMap, Agda.Interaction.Highlighting.Precise |
ToNLPat | Agda.TypeChecking.Rewriting.Clause |
toNLPat | Agda.TypeChecking.Rewriting.Clause |
TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyArgumentsToLeveledSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyArgumentsToUnivOmega | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyFields | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base.Warning |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
TooManyFields_ | Agda.Interaction.Options.Warnings |
TooManyPolarities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 (Data Constructor) | Agda.Syntax.TopLevelModuleName.Boot, Agda.Syntax.Common, Agda.Syntax.TopLevelModuleName |
2 (Type/Class) | Agda.Syntax.TopLevelModuleName |
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 |
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 |
topSort | Agda.Utils.Graph.TopSort |
topVarOcc | Agda.TypeChecking.Free.Lazy |
toReduceDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
toTermR | 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 |
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 |
translateRecordPatterns | 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 |
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 |
traversePatternM | Agda.Syntax.Internal.Pattern |
traverseTermM | Agda.Syntax.Internal.Generic |
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 |
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 |
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 |
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 |