Tag | Agda.Compiler.Epic.AuxAST |
takeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
takeEqualities | Agda.TypeChecking.Rules.LHS.Unify |
takeI | Agda.Syntax.Position, Agda.Interaction.GhciTop |
takenNameStr | Agda.Interaction.GhciTop |
takeP | Agda.Utils.Permutation |
takeTele | Agda.Compiler.Epic.Forcing |
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 | |
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, Agda.Interaction.GhciTop |
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.Syntax.Internal |
teleNames | Agda.TypeChecking.Telescope |
telePi | Agda.TypeChecking.Substitute |
telePi_ | Agda.TypeChecking.Substitute |
telePos | Agda.Compiler.Epic.Forcing |
Telescope | |
1 (Type/Class) | Agda.Syntax.Concrete |
2 (Type/Class) | Agda.Syntax.Internal |
3 (Type/Class) | Agda.Syntax.Abstract |
telFromList | Agda.Syntax.Internal |
tellEmacsToJumpToError | Agda.Interaction.GhciTop |
telToList | Agda.Syntax.Internal |
TelV | Agda.TypeChecking.Substitute |
telVars | Agda.TypeChecking.Substitute |
TelView | Agda.TypeChecking.Substitute |
telView | Agda.TypeChecking.Telescope |
telView' | Agda.TypeChecking.Substitute |
telViewM | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
telViewUpTo | Agda.TypeChecking.Telescope |
Term | |
1 (Type/Class) | Agda.Auto.NarrowingSearch |
2 (Data Constructor) | Agda.Auto.NarrowingSearch |
3 (Type/Class) | Agda.Syntax.Internal |
term | Agda.Compiler.MAlonzo.Compiler |
term' | Agda.Compiler.MAlonzo.Compiler |
TermConf | Agda.TypeChecking.Test.Generators |
TermConfiguration | Agda.TypeChecking.Test.Generators |
termDecls | Agda.Termination.TermCheck |
TermFreqs | |
1 (Type/Class) | Agda.TypeChecking.Test.Generators |
2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
termFreqs | Agda.TypeChecking.Test.Generators |
TermFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TermHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
terminates | Agda.Termination.Termination |
TerminationCheckFailed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
TerminationProblem | Agda.Interaction.Highlighting.Precise |
terminationProblems | Agda.Interaction.Imports |
TermLike | Agda.Syntax.Internal.Generic |
Testable | Agda.Utils.QuickCheck |
tests | |
1 (Function) | Agda.Utils.FileName, Agda.Interaction.FindFile |
2 (Function) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
3 (Function) | Agda.Utils.List |
4 (Function) | Agda.Interaction.Options |
5 (Function) | Agda.Interaction.Highlighting.Range |
6 (Function) | Agda.Interaction.Highlighting.Precise |
7 (Function) | Agda.Syntax.Parser.Parser |
8 (Function) | Agda.Termination.Semiring |
9 (Function) | Agda.Termination.SparseMatrix |
10 (Function) | Agda.Termination.CallGraph |
11 (Function) | Agda.Termination.Matrix |
12 (Function) | Agda.Utils.Either |
13 (Function) | Agda.Termination.Lexicographic |
14 (Function) | Agda.Termination.Termination |
15 (Function) | Agda.Utils.Warshall |
16 (Function) | Agda.TypeChecking.Tests |
17 (Function) | Agda.Interaction.Highlighting.Generate |
18 (Function) | Agda.Interaction.Highlighting.Emacs |
19 (Function) | Agda.Compiler.MAlonzo.Encode |
testSuite | Agda.Tests |
text | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
TextDetails | Agda.Utils.Pretty |
theCurrentFile | Agda.Interaction.GhciTop |
theDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
theFixity | Agda.Syntax.Fixity |
theInteractionPoints | Agda.Interaction.GhciTop |
theNotation | Agda.Syntax.Fixity |
theState | Agda.Interaction.GhciTop |
theTCState | Agda.Interaction.GhciTop |
theTelescope | Agda.Compiler.Epic.Forcing |
ThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
thingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
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 |
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, Agda.Interaction.GhciTop |
toAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
ToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
toConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
toConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
toggleImplicitArgs | Agda.Interaction.GhciTop |
toIFile | Agda.Interaction.FindFile |
TokComment | Agda.Syntax.Parser.Tokens |
TokDummy | Agda.Syntax.Parser.Tokens |
Token | Agda.Syntax.Parser.Tokens |
token | Agda.Syntax.Parser.LexActions |
TokenLength | Agda.Syntax.Parser.Alex |
tokensParser | |
1 (Function) | Agda.Syntax.Parser.Parser |
2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
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.Interaction.Highlighting.Range |
2 (Function) | Agda.Termination.CallGraph |
toLists | |
1 (Function) | Agda.Termination.SparseMatrix |
2 (Function) | Agda.Termination.Matrix |
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 |
topBindings | Agda.Compiler.Epic.CompileState |
topContext | Agda.Syntax.Parser.Monad |
TopCtx | Agda.Syntax.Fixity |
TopLevel | |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
topLevelDecls | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
TopLevelInfo | |
1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
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, Agda.Interaction.GhciTop |
topoSort | Agda.Utils.Permutation |
topSearch | Agda.Auto.NarrowingSearch |
top_command' | Agda.Interaction.GhciTop |
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, Agda.Interaction.GhciTop |
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 |
traceCall_ | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
traceFun | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
traceFun' | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
transitiveClosure | Agda.Utils.Graph |
translateCase | Agda.Compiler.Epic.Primitive |
translatedClause | Agda.Syntax.Internal |
translateDefn | Agda.Compiler.Epic.FromAgda |
translateRecordPatterns | 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 |
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 |
tryOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
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 |
TypeAndDef | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
typeCheck | Agda.Interaction.Imports |
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 |
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 |
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 |
typeOfSizeInf | Agda.TypeChecking.Rules.Builtin |
typeOfSizeSuc | Agda.TypeChecking.Rules.Builtin |
typeOfVar | Agda.TypeChecking.Coverage |
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 |