| 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 | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| Termination | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| 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 |
| 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 |
| 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 |
| testLub | Agda.TypeChecking.SizedTypes.WarshallSolver |
| tests | |
| 1 (Function) | Agda.Utils.Cluster |
| 2 (Function) | Agda.Utils.BiMap |
| 3 (Function) | Agda.Termination.Semiring |
| 4 (Function) | Agda.Utils.PartialOrd |
| 5 (Function) | Agda.Utils.Graph.AdjacencyMap |
| 6 (Function) | Agda.Utils.List |
| 7 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 8 (Function) | Agda.Utils.FileName, Agda.Interaction.FindFile |
| 9 (Function) | Agda.Syntax.Position |
| 10 (Function) | Agda.Utils.Warshall |
| 11 (Function) | Agda.Interaction.Highlighting.Range |
| 12 (Function) | Agda.Utils.Either |
| 13 (Function) | Agda.Utils.Favorites |
| 14 (Function) | Agda.TypeChecking.SizedTypes.Tests |
| 15 (Function) | Agda.Termination.SparseMatrix |
| 16 (Function) | Agda.Termination.Order |
| 17 (Function) | Agda.Termination.CallMatrix |
| 18 (Function) | Agda.Termination.CallGraph |
| 19 (Function) | Agda.Termination.Termination |
| 20 (Function) | Agda.Interaction.Options |
| 21 (Function) | Agda.Interaction.Highlighting.Precise |
| 22 (Function) | Agda.Syntax.Parser.Parser |
| 23 (Function) | Agda.TypeChecking.Irrelevance |
| 24 (Function) | Agda.Interaction.Highlighting.Emacs |
| 25 (Function) | Agda.Compiler.MAlonzo.Encode |
| 26 (Function) | Agda.TypeChecking.Tests |
| 27 (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 |
| 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 |
| 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 | Agda.Utils.Trie |
| 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 |
| 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.Graph.AdjacencyMap.Unidirectional |
| 5 (Function) | Agda.Utils.Favorites |
| 6 (Function) | Agda.Utils.Trie |
| 7 (Function) | Agda.Termination.CallMatrix |
| 8 (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 |
| 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 |
| 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 |
| 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 | 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 |
| typeCheck | Agda.Interaction.Imports |
| 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 |
| 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 |
| typesOfHiddenMetas | Agda.Interaction.BasicOps |
| typesOfVisibleMetas | Agda.Interaction.BasicOps |
| Typing | Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark |