Tactic | Agda.Syntax.Concrete |
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 |
takeP | Agda.Utils.Permutation |
takeRelevant | Agda.TypeChecking.MetaVars.Occurs |
takeTele | Agda.Compiler.Epic.Forcing |
takeWhileJust | Agda.Utils.List |
tallyDef | Agda.TypeChecking.MetaVars.Occurs |
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 |
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 |
tcProjectionNames | Agda.TypeChecking.Test.Generators |
tcSearch | Agda.Auto.Typecheck |
TCSt | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
Tel | |
1 (Type/Class) | Agda.Syntax.Concrete.Pretty |
2 (Data Constructor) | Agda.Syntax.Concrete.Pretty |
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 |
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.Abstract |
3 (Type/Class) | Agda.Syntax.Internal |
telFromList | Agda.TypeChecking.Substitute |
telFromList' | Agda.TypeChecking.Substitute |
TelHH | Agda.TypeChecking.Rules.LHS.Unify |
tellDirty | Agda.Utils.Update |
tellEmacsToJumpToError | Agda.Interaction.InteractionTop |
tellToUpdateHighlighting | Agda.Interaction.InteractionTop |
telToArgs | Agda.TypeChecking.Substitute |
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 |
TempInstanceTable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
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 |
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.Internal |
terM | Agda.Termination.Monad |
term | |
1 (Function) | Agda.Compiler.MAlonzo.Compiler |
2 (Function) | Agda.Compiler.JS.Compiler |
term' | Agda.Compiler.MAlonzo.Compiler |
terMaskArgs | Agda.Termination.Monad |
terMaskResult | Agda.Termination.Monad |
TermConf | Agda.TypeChecking.Test.Generators |
TermConfiguration | Agda.TypeChecking.Test.Generators |
TermDBP | Agda.Termination.Monad |
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 |
Terminating | Agda.Syntax.Common |
Termination | Agda.TypeChecking.Monad.Base.Benchmark, 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 |
TerminationCheckPragma | Agda.Syntax.Concrete |
TerminationError | |
1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TerminationMeasure | Agda.Syntax.Common |
TerminationProblem | Agda.Interaction.Highlighting.Precise |
TermLike | Agda.Syntax.Internal.Generic |
terModifyGuarded | Agda.Termination.Monad |
terModifyUsableVars | Agda.Termination.Monad |
terModifyUseSizeLt | Agda.Termination.Monad |
terMutual | Agda.Termination.Monad |
terPatterns | Agda.Termination.Monad |
terPatternsRaise | Agda.Termination.Monad |
terPiGuarded | Agda.Termination.Monad |
terRaise | Agda.Termination.Monad |
terSetCurrent | Agda.Termination.Monad |
terSetDelayed | Agda.Termination.Monad |
terSetGuarded | Agda.Termination.Monad |
terSetMaskArgs | Agda.Termination.Monad |
terSetMaskResult | Agda.Termination.Monad |
terSetPatterns | Agda.Termination.Monad |
terSetTarget | Agda.Termination.Monad |
terSetUsableVars | Agda.Termination.Monad |
terSetUseDotPatterns | Agda.Termination.Monad |
terSetUseSizeLt | Agda.Termination.Monad |
terSharp | 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 |
Testable | Agda.Utils.QuickCheck |
testChar | Agda.Utils.Char |
testLub | Agda.TypeChecking.SizedTypes.WarshallSolver |
tests | |
1 (Function) | Agda.Utils.Cluster |
2 (Function) | Agda.Utils.BiMap |
3 (Function) | Agda.Utils.Either |
4 (Function) | Agda.Termination.Semiring |
5 (Function) | Agda.Utils.PartialOrd |
6 (Function) | Agda.Utils.Graph.AdjacencyMap |
7 (Function) | Agda.Utils.FileName, Agda.Interaction.FindFile |
8 (Function) | Agda.Utils.Favorites |
9 (Function) | Agda.Utils.Bag |
10 (Function) | Agda.Utils.List |
11 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
12 (Function) | Agda.TypeChecking.SizedTypes.Tests |
13 (Function) | Agda.Syntax.Position |
14 (Function) | Agda.Interaction.Highlighting.Range |
15 (Function) | Agda.Utils.Warshall |
16 (Function) | Agda.Utils.Permutation.Tests |
17 (Function) | Agda.Termination.SparseMatrix |
18 (Function) | Agda.Termination.Order |
19 (Function) | Agda.Termination.CallMatrix |
20 (Function) | Agda.Termination.CallGraph |
21 (Function) | Agda.Termination.Termination |
22 (Function) | Agda.Interaction.Options |
23 (Function) | Agda.Interaction.Highlighting.Precise |
24 (Function) | Agda.Syntax.Parser.Parser |
25 (Function) | Agda.TypeChecking.Irrelevance |
26 (Function) | Agda.Interaction.Highlighting.Emacs |
27 (Function) | Agda.Compiler.MAlonzo.Encode |
28 (Function) | Agda.TypeChecking.Tests |
29 (Function) | Agda.Interaction.Highlighting.Generate |
testSplitTreePrinting | Agda.TypeChecking.Coverage.SplitTree |
testSuccs | Agda.TypeChecking.SizedTypes.WarshallSolver |
testSuite | Agda.Tests |
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 |
theCallGraph | Agda.Termination.CallGraph |
theConstraint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theCore | Agda.TypeChecking.Substitute |
theCurrentFile | Agda.Interaction.InteractionTop |
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theException | Agda.Utils.QuickCheck |
theFixity | Agda.Syntax.Fixity |
theInteractionPoints | Agda.Interaction.InteractionTop |
theNotation | Agda.Syntax.Fixity |
thenTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theSize | Agda.Utils.Size |
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 |
thread | Agda.Utils.Monad |
three | Agda.Utils.TestHelpers |
throwError | Agda.Utils.Except |
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 |
TLet | |
1 (Data Constructor) | Agda.Syntax.Concrete |
2 (Data Constructor) | Agda.Syntax.Abstract |
tlmname | Agda.Compiler.MAlonzo.Misc |
tlmodOf | Agda.Compiler.MAlonzo.Misc |
TMAll | Agda.Auto.Convert |
TMode | Agda.Auto.Convert |
to | Agda.Interaction.Highlighting.Range |
ToAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
toAbstract | Agda.Syntax.Translation.ConcreteToAbstract |
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 |
toDescList | Agda.Utils.VarSet |
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 |
toLazy | Agda.Utils.Maybe.Strict |
toList | |
1 (Function) | Agda.Utils.VarSet |
2 (Function) | Agda.Utils.HashMap |
3 (Function) | Agda.Utils.BiMap |
4 (Function) | Agda.Utils.Favorites |
5 (Function) | Agda.Utils.Bag |
6 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
7 (Function) | Agda.Utils.Trie |
8 (Function) | Agda.Termination.CallMatrix |
9 (Function) | Agda.Termination.CallGraph |
toLists | 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 |
TooFewArgumentsToPatternSynonym | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TooFewFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TooManyArgumentsInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TooManyFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
toOrderings | Agda.Utils.PartialOrd |
Top | |
1 (Type/Class) | Agda.TypeChecking.SizedTypes.Utils |
2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
top | Agda.TypeChecking.SizedTypes.Utils |
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 |
topLevelPath | Agda.Syntax.Translation.ConcreteToAbstract |
topLevelTheThing | Agda.Syntax.Translation.ConcreteToAbstract |
topoSort | Agda.Utils.Permutation |
topSearch | Agda.Auto.NarrowingSearch |
topSort | Agda.Syntax.Internal |
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.Abstract, Agda.Syntax.Internal |
toTree | Agda.TypeChecking.Coverage.SplitTree |
toTrees | Agda.TypeChecking.Coverage.SplitTree |
toVim | Agda.Interaction.Highlighting.Vim |
toWeight | Agda.TypeChecking.SizedTypes.WarshallSolver |
trace | Agda.TypeChecking.SizedTypes.Utils |
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 |
traceM | Agda.TypeChecking.SizedTypes.Utils |
traceSDoc | Agda.TypeChecking.Reduce.Monad |
traceSLn | Agda.TypeChecking.Reduce.Monad |
trampoline | Agda.Utils.Function |
trampolineM | Agda.Utils.Function |
trampolineWhile | Agda.Utils.Function |
trampolineWhileM | Agda.Utils.Function |
transClos | Agda.TypeChecking.SizedTypes.WarshallSolver |
transitiveClosure | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
transitiveClosure1 | |
1 (Function) | Agda.Utils.Graph.AdjacencyMap |
2 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
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 |
transposeEdge | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
Trav | Agda.Auto.NarrowingSearch |
traverse | |
1 (Function) | Agda.Utils.Bag |
2 (Function) | Agda.Auto.NarrowingSearch |
traverseExpr | |
1 (Function) | Agda.Syntax.Abstract.Views |
2 (Function) | Agda.Syntax.Concrete.Generic |
traverseF | Agda.Utils.Functor |
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 |
TruncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
truncateOffset | Agda.TypeChecking.SizedTypes.Syntax |
tryConversion | Agda.TypeChecking.Conversion |
tryOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
tryRecordType | Agda.TypeChecking.Records |
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 |
Type' | Agda.Syntax.Internal |
TypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
typeCheckMain | 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 |
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 |
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 |
typeError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
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 |
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 |
TypeSignatureOrInstanceBlock | Agda.Syntax.Concrete |
typesOfHiddenMetas | Agda.Interaction.BasicOps |
typesOfVisibleMetas | Agda.Interaction.BasicOps |
Typing | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |