Tag | |
1 (Type/Class) | Agda.Compiler.JS.Case |
2 (Data Constructor) | Agda.Compiler.JS.Case |
3 (Type/Class) | Agda.Compiler.Epic.Interface |
4 (Data Constructor) | Agda.Compiler.Epic.Interface |
tag | |
1 (Function) | Agda.Compiler.JS.Case |
2 (Function) | Agda.Compiler.JS.Compiler |
TagEq | Agda.Compiler.Epic.Injection |
Tagged | Agda.Compiler.JS.Case |
Tags | |
1 (Type/Class) | Agda.Compiler.Epic.Injection |
2 (Data Constructor) | Agda.Compiler.Epic.Injection |
tags | Agda.Compiler.JS.Case |
takeAwakeConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
takeEqualities | Agda.TypeChecking.Rules.LHS.Unify |
takeI | Agda.Syntax.Position |
takenNameStr | Agda.Interaction.InteractionTop |
takeP | Agda.Utils.Permutation |
takeRelevant | Agda.TypeChecking.MetaVars.Occurs |
takeTele | Agda.Compiler.Epic.Forcing |
tallyDef | Agda.TypeChecking.MetaVars.Occurs |
target | Agda.Termination.CallGraph |
TBind | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
tcargs | Agda.Auto.Typecheck |
tcConstructorNames | Agda.TypeChecking.Test.Generators |
tcDefinedNames | Agda.TypeChecking.Test.Generators |
TCEnv | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TCErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
tcErrString | Agda.TypeChecking.Errors |
tcExp | Agda.Auto.Typecheck |
tcFixSize | Agda.TypeChecking.Test.Generators |
tcFreeVariables | Agda.TypeChecking.Test.Generators |
tcFrequencies | Agda.TypeChecking.Test.Generators |
tcIsType | Agda.TypeChecking.Test.Generators |
tcLiterals | Agda.TypeChecking.Test.Generators |
TCM | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
tcSearch | Agda.Auto.Typecheck |
TCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Tele | Agda.Syntax.Internal |
teleArgNames | Agda.TypeChecking.Telescope |
teleArgs | Agda.TypeChecking.Telescope |
teleLam | Agda.TypeChecking.Substitute |
teleNames | Agda.TypeChecking.Telescope |
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.TypeChecking.Substitute |
TelHH | Agda.TypeChecking.Rules.LHS.Unify |
tellEmacsToJumpToError | Agda.Interaction.InteractionTop |
tellToUpdateHighlighting | Agda.Interaction.InteractionTop |
telToList | Agda.TypeChecking.Substitute |
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 |
TelViewHH | Agda.TypeChecking.Rules.LHS.Unify |
telViewUpTo | Agda.TypeChecking.Telescope |
telViewUpTo' | Agda.TypeChecking.Telescope |
telViewUpToHH | Agda.TypeChecking.Rules.LHS.Unify |
Term | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
3 (Type/Class) | Agda.Syntax.Internal |
term | |
1 (Function) | Agda.Compiler.MAlonzo.Compiler |
2 (Function) | Agda.Compiler.JS.Compiler |
term' | Agda.Compiler.MAlonzo.Compiler |
TermConf | Agda.TypeChecking.Test.Generators |
TermConfiguration | Agda.TypeChecking.Test.Generators |
termDecl | Agda.Termination.TermCheck |
termErrCalls | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
termErrFunctions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TermFreqs | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
termFreqs | Agda.TypeChecking.Test.Generators |
TermHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TermHH | Agda.TypeChecking.Rules.LHS.Unify |
terminates | Agda.Termination.Termination |
terminatesFilter | Agda.Termination.Termination |
TerminationCheckFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TerminationError | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TerminationProblem | Agda.Interaction.Highlighting.Precise |
terminationProblems | Agda.TypeChecking.Errors |
TermLike | Agda.Syntax.Internal.Generic |
Testable | Agda.Utils.QuickCheck |
tests | |
1 (Function) | Agda.Termination.Semiring |
2 (Function) | Agda.Termination.Matrix |
3 (Function) | Agda.Utils.List |
4 (Function) | Agda.Utils.Either |
5 (Function) | Agda.Termination.SparseMatrix |
6 (Function) | Agda.Termination.CallGraph |
7 (Function) | Agda.Termination.Lexicographic |
8 (Function) | Agda.Termination.Termination |
9 (Function) | Agda.Utils.FileName, Agda.Interaction.FindFile |
10 (Function) | Agda.Utils.Graph |
11 (Function) | Agda.Interaction.Options |
12 (Function) | Agda.Syntax.Position |
13 (Function) | Agda.Utils.Warshall |
14 (Function) | Agda.Interaction.Highlighting.Range |
15 (Function) | Agda.Interaction.Highlighting.Precise |
16 (Function) | Agda.Syntax.Parser.Parser |
17 (Function) | Agda.TypeChecking.Irrelevance |
18 (Function) | Agda.Interaction.Highlighting.Emacs |
19 (Function) | Agda.Interaction.Highlighting.Generate |
20 (Function) | Agda.Compiler.MAlonzo.Encode |
21 (Function) | Agda.TypeChecking.Tests |
testSplitTreePrinting | Agda.TypeChecking.Coverage.SplitTree |
testSuite | Agda.Tests |
text | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
TextDetails | Agda.Utils.Pretty |
thd3 | Agda.Utils.Tuple |
theConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theCurrentFile | Agda.Interaction.InteractionTop |
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theFixity | Agda.Syntax.Fixity |
theInteractionPoints | Agda.Interaction.InteractionTop |
theNotation | Agda.Syntax.Fixity |
thenTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
thread | Agda.Utils.Monad |
three | Agda.Utils.TestHelpers |
throwException | Agda.TypeChecking.Monad.Exception |
throwImpossible | Agda.Utils.Impossible |
tick | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
tickMax | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
tickN | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
tlmname | Agda.Compiler.MAlonzo.Misc |
tlmodOf | Agda.Compiler.MAlonzo.Misc |
TMAll | Agda.Auto.Convert |
TMode | Agda.Auto.Convert |
TNoBind | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
to | Agda.Interaction.Highlighting.Range |
ToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
toAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete |
toConcrete | Agda.Syntax.Translation.AbstractToConcrete |
toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete |
ToggleImplicitArgs | Agda.Interaction.InteractionTop |
toIFile | Agda.Interaction.FindFile |
TokComment | Agda.Syntax.Parser.Tokens |
TokDummy | Agda.Syntax.Parser.Tokens |
Token | Agda.Syntax.Parser.Tokens |
token | |
1 (Function) | Agda.Compiler.JS.Parser |
2 (Function) | Agda.Syntax.Parser.LexActions |
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 |
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 |
toList | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Termination.CallGraph |
toLists | |
1 (Function) | Agda.Termination.Matrix |
2 (Function) | Agda.Termination.SparseMatrix |
TOM | Agda.Auto.Convert |
toMap | Agda.Interaction.Highlighting.Precise |
tomy | Agda.Auto.Convert |
tomyBody | Agda.Auto.Convert |
tomyClause | Agda.Auto.Convert |
tomyClauses | Agda.Auto.Convert |
tomyExp | Agda.Auto.Convert |
tomyExps | Agda.Auto.Convert |
tomyIneq | Agda.Auto.Convert |
tomyPat | Agda.Auto.Convert |
tomyType | Agda.Auto.Convert |
TooFewFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TooManyArgumentsInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TooManyFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Top | Agda.TypeChecking.MetaVars.Occurs |
topBindings | Agda.Compiler.Epic.CompileState |
topContext | Agda.Syntax.Parser.Monad |
TopCtx | Agda.Syntax.Fixity |
TopLevel | |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract |
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract |
topLevel | Agda.Compiler.JS.Parser |
topLevelDecls | 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 |
topoSort | Agda.Utils.Permutation |
topSearch | Agda.Auto.NarrowingSearch |
topSort | Agda.Syntax.Internal |
toSubscriptDigit | Agda.Utils.Suffix |
ToTerm | Agda.TypeChecking.Primitive |
toTerm | Agda.TypeChecking.Primitive |
toTopLevelModuleName | |
1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract |
toTree | Agda.TypeChecking.Coverage.SplitTree |
toTrees | Agda.TypeChecking.Coverage.SplitTree |
toVim | Agda.Interaction.Highlighting.Vim |
traceCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceCallCPS | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceCallCPS_ | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceCallE | Agda.TypeChecking.Rules.Term |
traceCallM | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceCall_ | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceFun | Agda.TypeChecking.Reduce |
traceFun' | Agda.TypeChecking.Reduce |
trailingImplicits | Agda.TypeChecking.Rules.Def |
transitiveClosure | Agda.Utils.Graph |
transitiveClosure1 | Agda.Utils.Graph |
translateCase | Agda.Compiler.Epic.Primitive |
translateCompiledClauses | Agda.TypeChecking.RecordPatterns |
translateCopatternClauses | Agda.Syntax.Abstract.Copatterns |
translateDefn | Agda.Compiler.Epic.FromAgda |
translateRecordPatterns | Agda.TypeChecking.RecordPatterns |
translateSplitTree | Agda.TypeChecking.RecordPatterns |
transpose | Agda.Termination.SparseMatrix |
Trav | Agda.Auto.NarrowingSearch |
traverse | Agda.Auto.NarrowingSearch |
traversePi | Agda.Auto.Typecheck |
traverseTerm | Agda.Syntax.Internal.Generic |
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 |
treatAbstractly' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
Trie | Agda.Utils.Trie |
trivial | Agda.TypeChecking.SizedTypes |
trivialHH | Agda.TypeChecking.Rules.LHS.Unify |
trueCondition | Agda.TypeChecking.MetaVars |
tryOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
trySizeUniv | Agda.TypeChecking.SizedTypes |
tset | Agda.TypeChecking.Primitive |
tvaldecl | Agda.Compiler.MAlonzo.Compiler |
two | Agda.Utils.TestHelpers |
Type | |
1 (Data Constructor) | Agda.Auto.Syntax |
2 (Data Constructor) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Internal |
typeCheck | Agda.Interaction.Imports |
TypeChecks | Agda.Interaction.Highlighting.Precise |
TypeCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TypedAssign | Agda.Interaction.BasicOps |
TypedBinding | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
TypedBindings | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Concrete |
3 (Type/Class) | Agda.Syntax.Abstract |
4 (Data Constructor) | Agda.Syntax.Abstract |
typeDontCare | Agda.Syntax.Internal |
TypeError | |
1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
typeError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
typeFromProblem | Agda.TypeChecking.Rules.LHS.ProblemRest |
TypeHH | Agda.TypeChecking.Rules.LHS.Unify |
typeIn | Agda.Interaction.CommandLine.CommandLine |
typeInCurrent | Agda.Interaction.BasicOps |
typeInMeta | Agda.Interaction.BasicOps |
typeInType | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
typeName | Agda.TypeChecking.Level |
typeOf | Agda.Interaction.CommandLine.CommandLine |
typeOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
typeOfBV' | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
typeOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
typeOfFlat | Agda.TypeChecking.Rules.Builtin.Coinduction |
typeOfInf | Agda.TypeChecking.Rules.Builtin.Coinduction |
typeOfMeta | Agda.Interaction.BasicOps |
typeOfMetaMI | Agda.Interaction.BasicOps |
typeOfSharp | Agda.TypeChecking.Rules.Builtin.Coinduction |
TypeSig | Agda.Syntax.Concrete |
TypeSignature | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Abstract |
typesOfHiddenMetas | Agda.Interaction.BasicOps |
typesOfVisibleMetas | Agda.Interaction.BasicOps |