| !!! | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| $!! | Agda.Syntax.Strict |
| $$ | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| $$$ | Agda.Syntax.Concrete.Operators.Parser |
| $+$ | Agda.Utils.Pretty |
| &&- | Agda.Compiler.Epic.Erasure |
| +++ | Agda.Utils.ReadP |
| -*- | Agda.Utils.Tuple |
| --> | Agda.TypeChecking.Primitive |
| .&&. | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.Syntax.Parser.Alex |
| .&. | Agda.Utils.QuickCheck |
| .*. | Agda.Termination.CallGraph |
| .||. | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.Syntax.Parser.Alex |
| /\ | |
| 1 (Function) | Agda.Utils.Tuple |
| 2 (Function) | Agda.TypeChecking.Polarity |
| :-> | Agda.TypeChecking.CompiledClause |
| <#> | Agda.TypeChecking.Primitive |
| <$> | Agda.Utils.Monad |
| <*> | Agda.Utils.Monad |
| <++ | Agda.Utils.ReadP |
| <+> | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| <.> | Agda.Utils.Monad |
| <> | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| <@> | Agda.TypeChecking.Primitive |
| =: | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| =:= | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| === | Agda.Utils.FileName |
| ==> | Agda.Utils.QuickCheck |
| >*< | |
| 1 (Function) | Agda.Termination.CallGraph |
| 2 (Function) | Agda.TypeChecking.Positivity |
| >+< | Agda.TypeChecking.Positivity |
| >< | Agda.Utils.QuickCheck |
| A | Agda.Interaction.GhciTop |
| abort | Agda.TypeChecking.MetaVars.Occurs |
| AbortAssign | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| abortAssign | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| Abs | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| absApp | Agda.TypeChecking.Substitute |
| absBody | Agda.Syntax.Internal |
| abslamvarname | Agda.Auto.Convert |
| AbsModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbsName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| absName | Agda.Syntax.Internal |
| absolute | Agda.Utils.FileName |
| AbsolutePath | Agda.Utils.FileName |
| abspatvarname | Agda.Auto.CaseSplit |
| AbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| Abstract | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.TypeChecking.Substitute |
| abstract | Agda.TypeChecking.Substitute |
| abstractArgs | Agda.TypeChecking.Substitute |
| AbstractDef | Agda.Syntax.Common |
| AbstractMode | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AbstractModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbstractName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AbstractRHS | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| AbstractTerm | Agda.TypeChecking.Abstract |
| abstractTerm | Agda.TypeChecking.Abstract |
| abstractToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| abstractToConcreteCtx | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| abstractToConcrete_ | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| Absurd | Agda.Syntax.Concrete |
| AbsurdLam | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdLambda | Agda.Auto.Syntax |
| AbsurdP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| AbsurdPatternRequiresNoRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AbsurdRHS | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Access | Agda.Syntax.Common |
| actOnMeta | Agda.Interaction.CommandLine.CommandLine |
| actualConstructor | Agda.TypeChecking.Rules.Def |
| add | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| 3 (Function) | Agda.Termination.Matrix |
| addblk | Agda.Auto.Typecheck |
| addColumn | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| addConstant | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addConstraint | Agda.Utils.Warshall |
| addConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| addCtx | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtxs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addCtxTel | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addDataDecl | Agda.Compiler.Epic.CompileState |
| addDecl | Agda.Interaction.BasicOps |
| addDefName | Agda.Compiler.Epic.CompileState |
| addDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addEdge | Agda.Utils.Warshall |
| addend | Agda.Auto.Typecheck |
| addEpicCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addEquality | Agda.TypeChecking.Rules.LHS.Unify |
| AddExtraRef | Agda.Auto.NarrowingSearch |
| addFinalNewLine | Agda.Utils.String |
| addFlex | Agda.Utils.Warshall |
| addForcingAnnotations | Agda.TypeChecking.Forcing |
| addHaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addHaskellImport | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| addHaskellType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addImport | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| addImportCycleCheck | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| addImportedThings | Agda.Interaction.Imports |
| addInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| addLetBinding | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| addModuleToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNamesToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNameToScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| addNewConstraints | Agda.TypeChecking.Constraints |
| addNode | Agda.Utils.Warshall |
| addRow | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| addSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| addSuffix | Agda.Utils.Suffix |
| addtrailingargs | Agda.Auto.Syntax |
| ADef | Agda.TypeChecking.Positivity |
| AdjList | Agda.Utils.Warshall |
| agdaTermType | Agda.TypeChecking.Quote |
| ALConPar | Agda.Auto.Syntax |
| ALCons | Agda.Auto.Syntax |
| AlexEOF | Agda.Syntax.Parser.Lexer |
| AlexError | Agda.Syntax.Parser.Lexer |
| alexGetChar | Agda.Syntax.Parser.Alex |
| AlexInput | |
| 1 (Type/Class) | Agda.Syntax.Parser.Alex |
| 2 (Data Constructor) | Agda.Syntax.Parser.Alex |
| alexInputPrevChar | Agda.Syntax.Parser.Alex |
| AlexReturn | Agda.Syntax.Parser.Lexer |
| alexScanUser | Agda.Syntax.Parser.Lexer |
| AlexSkip | Agda.Syntax.Parser.Lexer |
| AlexToken | Agda.Syntax.Parser.Lexer |
| align | Agda.Utils.Pretty |
| allEqual | Agda.Utils.List |
| allHoles | Agda.Syntax.Internal.Pattern |
| allHolesWithContents | Agda.Syntax.Internal.Pattern |
| allMetaKinds | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| allNames | Agda.Syntax.Abstract |
| allNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| alloc | Agda.Utils.Pointer |
| allPaths | Agda.Utils.Graph |
| allRight | Agda.Utils.Either |
| allThingsInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| allVars | Agda.TypeChecking.Free |
| ALNil | Agda.Auto.Syntax |
| ALProj | Agda.Auto.Syntax |
| alreadyVisited | Agda.Interaction.Imports |
| Ambiguous | Agda.Interaction.FindFile |
| AmbiguousModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbiguousQName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| AmbiguousTopLevelModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| AmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| amodName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| anameKind | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| anameName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| AnArg | Agda.TypeChecking.Positivity |
| And | Agda.Auto.NarrowingSearch |
| AnyWhere | Agda.Syntax.Concrete |
| APatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| App | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.TypeChecking.EtaContract |
| appBrackets | Agda.Syntax.Fixity |
| Application | Agda.Syntax.Abstract.Views |
| Apply | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Type/Class) | Agda.TypeChecking.Substitute |
| apply | Agda.TypeChecking.Substitute |
| applyImportDirective | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| applyImportDirectiveM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| applyperm | Agda.Auto.CaseSplit |
| applyRelevanceToContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| applySection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| AppP | Agda.Syntax.Concrete |
| appP | Agda.Syntax.Concrete.Operators.Parser |
| apps | |
| 1 (Function) | Agda.Compiler.Epic.AuxAST |
| 2 (Function) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| AppV | Agda.Syntax.Concrete.Operators.Parser |
| AppView | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract.Views |
| appView | |
| 1 (Function) | Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Views |
| Arbitrary | Agda.Utils.QuickCheck |
| arbitrary | Agda.Utils.QuickCheck |
| arbitraryBoundedIntegral | Agda.Utils.QuickCheck |
| arbitraryBoundedRandom | Agda.Utils.QuickCheck |
| arbitrarySizedBoundedIntegral | Agda.Utils.QuickCheck |
| arbitrarySizedFractional | Agda.Utils.QuickCheck |
| arbitrarySizedIntegral | Agda.Utils.QuickCheck |
| Arc | Agda.Utils.Warshall |
| Arg | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| argH | Agda.TypeChecking.Primitive |
| argHiding | Agda.Syntax.Common |
| argIsDef | Agda.Compiler.Epic.NatDetection |
| ArgList | Agda.Auto.Syntax |
| argN | Agda.TypeChecking.Primitive |
| argName | Agda.Syntax.Internal |
| ArgNode | Agda.TypeChecking.Positivity |
| ArgPat | Agda.TypeChecking.With |
| argpatts | Agda.Compiler.MAlonzo.Compiler |
| argRelevance | Agda.Syntax.Common |
| Args | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| 3 (Type/Class) | Agda.Syntax.Internal |
| ArgsCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ArgumentCtx | Agda.Syntax.Fixity |
| ArgumentTo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Arity | Agda.Syntax.Common |
| arity | Agda.Syntax.Internal |
| arrow | Agda.Syntax.Concrete.Pretty |
| As | Agda.Syntax.Concrete |
| AsB | Agda.TypeChecking.Rules.LHS |
| AsBinding | Agda.TypeChecking.Rules.LHS |
| AsIs | Agda.Interaction.BasicOps |
| AsName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| asName | Agda.Syntax.Concrete |
| AsP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Aspect | Agda.Interaction.Highlighting.Precise |
| aspect | Agda.Interaction.Highlighting.Precise |
| asRange | Agda.Syntax.Concrete |
| Assign | Agda.Interaction.BasicOps |
| assignS | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| assignSort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| assignTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| assignV | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| associative | Agda.Utils.TestHelpers |
| asView | Agda.TypeChecking.Rules.LHS.Split |
| atomP | Agda.Syntax.Concrete.Operators.Parser |
| atTopLevel | Agda.Interaction.BasicOps |
| auto | Agda.Auto.Auto |
| axEpDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| axHsDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Axiom | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| axiomName | Agda.Syntax.Abstract |
| B | Agda.Utils.Map |
| Backend | Agda.Interaction.GhciTop |
| backupPos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| BadImplicits | Agda.TypeChecking.Implicit |
| begin | Agda.Syntax.Parser.LexActions |
| beginningOf | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| beginningOfFile | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| begin_ | Agda.Syntax.Parser.LexActions |
| betareduce | Agda.Auto.CaseSplit |
| between | Agda.Utils.ReadP |
| BinAppView | Agda.TypeChecking.EtaContract |
| binAppView | Agda.TypeChecking.EtaContract |
| Bind | Agda.Syntax.Internal |
| bindAsPatterns | Agda.TypeChecking.Rules.LHS |
| bindBuiltin | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinBool | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinCons | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinDummyConstructor | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinEquality | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinFlat | Agda.TypeChecking.Rules.Builtin.Coinduction |
| bindBuiltinInf | Agda.TypeChecking.Rules.Builtin.Coinduction |
| bindBuiltinLevelSuc | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinLevelZero | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinName | Agda.TypeChecking.Monad.Builtin |
| bindBuiltinNil | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinPrimitive | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinRefl | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinSharp | Agda.TypeChecking.Rules.Builtin.Coinduction |
| bindBuiltinSuc | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinSuc' | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinType | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinType1 | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinZero | Agda.TypeChecking.Rules.Builtin |
| bindBuiltinZero' | Agda.TypeChecking.Rules.Builtin |
| bindConstructor | Agda.TypeChecking.Rules.Builtin |
| BindHole | Agda.Syntax.Notation |
| bindLHSVars | Agda.TypeChecking.Rules.LHS |
| bindModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| bindName | Agda.Syntax.Scope.Monad |
| bindParameters | Agda.TypeChecking.Rules.Data |
| bindPostulate | Agda.TypeChecking.Rules.Builtin |
| bindPostulatedName | Agda.TypeChecking.Rules.Builtin |
| bindPrimitive | Agda.TypeChecking.Monad.Builtin |
| bindQModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| bindToConcrete | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| bindVariable | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| binop | Agda.Syntax.Concrete.Operators.Parser |
| Blind | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| BlkInfo | Agda.Auto.NarrowingSearch |
| Block | Agda.TypeChecking.Coverage.Match |
| Blocked | |
| 1 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| blocked | Agda.Syntax.Internal |
| BlockedConst | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| BlockedLevel | Agda.TypeChecking.Level |
| blockingMeta | Agda.Syntax.Internal |
| blockOfLines | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| blockTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| bltQual | Agda.Compiler.MAlonzo.Misc |
| bltQual' | Agda.Compiler.MAlonzo.Primitives |
| BName | Agda.Syntax.Concrete |
| bnameFixity | Agda.Syntax.Concrete |
| Body | Agda.Syntax.Internal |
| bol | Agda.Syntax.Parser.Lexer |
| boolPrimTF | Agda.Compiler.Epic.Primitive |
| boolSemiring | Agda.Termination.Semiring |
| BothWithAndRHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Bound | Agda.Interaction.Highlighting.Precise |
| BoundName | Agda.Syntax.Concrete |
| boundName | Agda.Syntax.Concrete |
| braces | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| braces' | Agda.Syntax.Concrete.Pretty |
| bracket | Agda.Utils.Monad |
| brackets | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Branch | |
| 1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| Branches | Agda.TypeChecking.CompiledClause |
| brExpr | Agda.Compiler.Epic.AuxAST |
| BrInt | Agda.Compiler.Epic.AuxAST |
| brInt | Agda.Compiler.Epic.AuxAST |
| brName | Agda.Compiler.Epic.AuxAST |
| brTag | Agda.Compiler.Epic.AuxAST |
| brVars | Agda.Compiler.Epic.AuxAST |
| buildClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| buildConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| buildGraph | Agda.Utils.Warshall |
| buildInterface | Agda.Interaction.Imports |
| buildList | Agda.TypeChecking.Primitive |
| buildMPatterns | Agda.TypeChecking.Coverage.Match |
| buildOccurrenceGraph | Agda.TypeChecking.Positivity |
| buildWithFunction | Agda.TypeChecking.With |
| Builtin | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| builtinAgdaTerm | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermCon | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermDef | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermLam | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
| builtinAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
| builtinArg | Agda.TypeChecking.Monad.Builtin |
| builtinArgArg | Agda.TypeChecking.Monad.Builtin |
| builtinBool | Agda.TypeChecking.Monad.Builtin |
| builtinChar | Agda.TypeChecking.Monad.Builtin |
| builtinCons | Agda.TypeChecking.Monad.Builtin |
| builtinConstructors | Agda.TypeChecking.Rules.Builtin |
| builtinDatatypes | Agda.TypeChecking.Rules.Builtin |
| builtinEquality | Agda.TypeChecking.Monad.Builtin |
| builtinFalse | Agda.TypeChecking.Monad.Builtin |
| builtinFlat | Agda.TypeChecking.Monad.Builtin |
| builtinFloat | Agda.TypeChecking.Monad.Builtin |
| builtinInf | Agda.TypeChecking.Monad.Builtin |
| BuiltinInParameterisedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| builtinInteger | Agda.TypeChecking.Monad.Builtin |
| builtinIO | Agda.TypeChecking.Monad.Builtin |
| builtinLevel | Agda.TypeChecking.Monad.Builtin |
| builtinLevelKit | Agda.TypeChecking.Level |
| builtinLevelMax | Agda.TypeChecking.Monad.Builtin |
| builtinLevelSuc | Agda.TypeChecking.Monad.Builtin |
| builtinLevelZero | Agda.TypeChecking.Monad.Builtin |
| builtinList | Agda.TypeChecking.Monad.Builtin |
| BuiltinMustBeConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| builtinNat | Agda.TypeChecking.Monad.Builtin |
| builtinNatDivSucAux | Agda.TypeChecking.Monad.Builtin |
| builtinNatEquals | Agda.TypeChecking.Monad.Builtin |
| builtinNatLess | Agda.TypeChecking.Monad.Builtin |
| builtinNatMinus | Agda.TypeChecking.Monad.Builtin |
| builtinNatModSucAux | Agda.TypeChecking.Monad.Builtin |
| builtinNatPlus | Agda.TypeChecking.Monad.Builtin |
| builtinNatTimes | Agda.TypeChecking.Monad.Builtin |
| builtinNil | Agda.TypeChecking.Monad.Builtin |
| builtinPostulates | Agda.TypeChecking.Rules.Builtin |
| BuiltinPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| builtinPrimitives | Agda.TypeChecking.Rules.Builtin |
| builtinQName | Agda.TypeChecking.Monad.Builtin |
| builtinRefl | Agda.TypeChecking.Monad.Builtin |
| builtinSharp | Agda.TypeChecking.Monad.Builtin |
| builtinSize | Agda.TypeChecking.Monad.Builtin |
| builtinSizeInf | Agda.TypeChecking.Monad.Builtin |
| builtinSizeSuc | Agda.TypeChecking.Monad.Builtin |
| builtinString | Agda.TypeChecking.Monad.Builtin |
| builtinSuc | Agda.TypeChecking.Monad.Builtin |
| BuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| builtinTrue | Agda.TypeChecking.Monad.Builtin |
| builtinTypes | Agda.TypeChecking.Monad.Builtin |
| builtinZero | Agda.TypeChecking.Monad.Builtin |
| CAction | Agda.Auto.Syntax |
| calc | Agda.Auto.NarrowingSearch |
| calcEqRState | Agda.Auto.Typecheck |
| CALConcat | Agda.Auto.Syntax |
| Call | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.Termination.CallGraph |
| 3 (Data Constructor) | Agda.Termination.CallGraph |
| callGHC | Agda.Compiler.MAlonzo.Compiler |
| CallGraph | Agda.Termination.CallGraph |
| callGraphInvariant | Agda.Termination.CallGraph |
| callInvariant | Agda.Termination.CallGraph |
| CallMatrix | |
| 1 (Type/Class) | Agda.Termination.CallGraph |
| 2 (Data Constructor) | Agda.Termination.CallGraph |
| callMatrixInvariant | Agda.Termination.CallGraph |
| calls | Agda.Termination.Lexicographic |
| CALNil | Agda.Auto.Syntax |
| canonicalName | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| CantSplit | Agda.TypeChecking.Coverage |
| Case | |
| 1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.TypeChecking.CompiledClause |
| 3 (Type/Class) | Agda.TypeChecking.CompiledClause |
| caseSplitSearch | Agda.Auto.CaseSplit |
| caseSplitSearch' | Agda.Auto.CaseSplit |
| cat | Agda.Utils.Pretty |
| catchAll | Agda.TypeChecking.CompiledClause |
| catchAllBranch | Agda.TypeChecking.CompiledClause |
| catchConstraint | Agda.TypeChecking.Constraints |
| catchError_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| catchException | Agda.TypeChecking.Monad.Exception |
| catchImpossible | Agda.Utils.Impossible |
| categorizedecl | Agda.Auto.Syntax |
| catMaybes | Agda.Utils.Maybe |
| cdcont | Agda.Auto.Syntax |
| cddeffreevars | Agda.Auto.Syntax |
| cdecl | Agda.Compiler.MAlonzo.Compiler |
| cdname | Agda.Auto.Syntax |
| cdorigin | Agda.Auto.Syntax |
| cdtype | Agda.Auto.Syntax |
| CExp | Agda.Auto.Syntax |
| chainl | Agda.Utils.ReadP |
| chainl1 | Agda.Utils.ReadP |
| chainl1' | Agda.Syntax.Concrete.Operators.Parser |
| chainr | Agda.Utils.ReadP |
| chainr1 | Agda.Utils.ReadP |
| chainr1' | Agda.Syntax.Concrete.Operators.Parser |
| char | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Utils.ReadP |
| chatty | Agda.Utils.QuickCheck |
| checkArgs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| CheckArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkArguments | Agda.TypeChecking.Rules.Term |
| checkArguments' | Agda.TypeChecking.Rules.Term |
| checkArguments_ | Agda.TypeChecking.Rules.Term |
| checkAxiom | Agda.TypeChecking.Rules.Decl |
| CheckClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkClause | Agda.TypeChecking.Rules.Def |
| CheckConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkConstructor | Agda.TypeChecking.Rules.Data |
| checkConstructorApplication | Agda.TypeChecking.Rules.Term |
| checkConstructorType | Agda.Compiler.MAlonzo.Compiler |
| checkCover | Agda.Compiler.MAlonzo.Compiler |
| checkCoverage | Agda.TypeChecking.Coverage |
| CheckDataDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkDataDef | Agda.TypeChecking.Rules.Data |
| checkDecl | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkDecls | Agda.TypeChecking.Rules.Decl, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkDefinition | Agda.TypeChecking.Rules.Decl |
| CheckDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkDotPattern | Agda.TypeChecking.Rules.LHS |
| checkeliminand | Agda.Auto.Typecheck |
| checkEqualities | Agda.TypeChecking.Rules.LHS.Unify |
| CheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
| checkForImportCycle | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| CheckFunDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkFunDef | Agda.TypeChecking.Rules.Def |
| checkHeadApplication | Agda.TypeChecking.Rules.Term |
| checkImport | Agda.TypeChecking.Rules.Decl |
| checkInjectivity | Agda.TypeChecking.Injectivity |
| checkLeftHandSide | Agda.TypeChecking.Rules.LHS |
| CheckLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkLetBinding | Agda.TypeChecking.Rules.Term |
| checkLetBindings | Agda.TypeChecking.Rules.Term |
| checkLiteral | Agda.TypeChecking.Rules.Term |
| checkModuleArity | Agda.TypeChecking.Rules.Decl |
| checkModuleName | Agda.Interaction.FindFile |
| checkMutual | Agda.TypeChecking.Rules.Decl |
| checkOpts | Agda.Interaction.Options |
| CheckPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckPatternShadowing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CheckPragma | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkPragma | Agda.TypeChecking.Rules.Decl |
| CheckPrimitive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkPrimitive | Agda.TypeChecking.Rules.Decl |
| CheckRecDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkRecDef | Agda.TypeChecking.Rules.Record |
| checkRecordProjections | Agda.TypeChecking.Rules.Record |
| checkSection | Agda.TypeChecking.Rules.Decl |
| CheckSectionApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| checkSectionApplication | Agda.TypeChecking.Rules.Decl |
| checkSizeIndex | Agda.TypeChecking.Polarity |
| checkStrictlyPositive | Agda.TypeChecking.Positivity |
| checkTelescope | Agda.TypeChecking.Rules.Term |
| checkTelescope_ | Agda.TypeChecking.Rules.Term |
| checkTypedBinding | Agda.TypeChecking.Rules.Term |
| checkTypedBindings | Agda.TypeChecking.Rules.Term |
| checkTypedBindings_ | Agda.TypeChecking.Rules.Term |
| checkTypedBinding_ | Agda.TypeChecking.Rules.Term |
| checkTypeOfMain | Agda.Compiler.MAlonzo.Primitives |
| checkTypeSignature | Agda.TypeChecking.Rules.Decl |
| checkWhere | Agda.TypeChecking.Rules.Def |
| checkWithFunction | Agda.TypeChecking.Rules.Def |
| Choice | Agda.Auto.NarrowingSearch |
| choice | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.TypeChecking.Coverage.Match |
| choose | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.Auto.NarrowingSearch |
| choosePrioMeta | Agda.Auto.NarrowingSearch |
| chop | Agda.Utils.List |
| Chr | Agda.Utils.Pretty |
| Cl | Agda.TypeChecking.CompiledClause |
| ClashingDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingFileNamesFor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ClashingModuleImport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| classify | Agda.Utils.QuickCheck |
| Clause | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Type/Class) | Agda.Syntax.Abstract |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| 6 (Type/Class) | Agda.Syntax.Concrete.Definitions |
| 7 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| clause | Agda.Compiler.MAlonzo.Compiler |
| ClauseBody | Agda.Syntax.Internal |
| clauseBody | Agda.Syntax.Internal |
| clausebody | Agda.Compiler.MAlonzo.Compiler |
| clausePats | Agda.Syntax.Internal |
| clausePerm | Agda.Syntax.Internal |
| clauseRange | Agda.Syntax.Internal |
| Clauses | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| clausesAbove | Agda.Compiler.Epic.Forcing |
| clauseTel | Agda.Syntax.Internal |
| clauseToFix | Agda.Compiler.Epic.Forcing |
| clearMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| clEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Clos | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| closeBrace | Agda.Syntax.Parser.Layout |
| ClosedLevel | Agda.TypeChecking.Level |
| closify | Agda.Auto.Syntax |
| Closure | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Cls | Agda.TypeChecking.CompiledClause |
| clScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| clValue | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cm | Agda.Termination.CallGraph |
| cmd_auto | Agda.Interaction.GhciTop |
| cmd_compile | Agda.Interaction.GhciTop |
| cmd_compute | Agda.Interaction.GhciTop |
| cmd_compute_toplevel | Agda.Interaction.GhciTop |
| cmd_constraints | Agda.Interaction.GhciTop |
| cmd_context | Agda.Interaction.GhciTop |
| cmd_give | Agda.Interaction.GhciTop |
| cmd_goal_type | Agda.Interaction.GhciTop |
| cmd_goal_type_context | Agda.Interaction.GhciTop |
| cmd_goal_type_context_and | Agda.Interaction.GhciTop |
| cmd_goal_type_context_infer | Agda.Interaction.GhciTop |
| cmd_infer | Agda.Interaction.GhciTop |
| cmd_infer_toplevel | Agda.Interaction.GhciTop |
| cmd_intro | Agda.Interaction.GhciTop |
| cmd_load | Agda.Interaction.GhciTop |
| cmd_load' | Agda.Interaction.GhciTop |
| cmd_make_case | Agda.Interaction.GhciTop |
| cmd_metas | Agda.Interaction.GhciTop |
| cmd_refine | Agda.Interaction.GhciTop |
| cmd_refine_or_intro | Agda.Interaction.GhciTop |
| cmd_show_module_contents | Agda.Interaction.GhciTop |
| cmd_show_module_contents_toplevel | Agda.Interaction.GhciTop |
| cmd_solveAll | Agda.Interaction.GhciTop |
| cmd_write_highlighting_info | Agda.Interaction.GhciTop |
| CMFBlocked | Agda.Auto.Typecheck |
| CMFFlex | Agda.Auto.Typecheck |
| CMFlex | |
| 1 (Type/Class) | Agda.Auto.Typecheck |
| 2 (Data Constructor) | Agda.Auto.Typecheck |
| CMFSemi | Agda.Auto.Typecheck |
| CMode | Agda.Auto.Typecheck |
| CmpEq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpInType | Agda.Interaction.BasicOps |
| CmpLeq | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CmpLevels | Agda.Interaction.BasicOps |
| CmpSorts | Agda.Interaction.BasicOps |
| CmpTeles | Agda.Interaction.BasicOps |
| CmpTerms | Agda.Interaction.BasicOps |
| CmpTypes | Agda.Interaction.BasicOps |
| CMRigid | Agda.Auto.Typecheck |
| cnvh | Agda.Auto.Convert |
| CoArbitrary | Agda.Utils.QuickCheck |
| coarbitrary | Agda.Utils.QuickCheck |
| coarbitraryIntegral | Agda.Utils.QuickCheck |
| coarbitraryReal | Agda.Utils.QuickCheck |
| coarbitraryShow | Agda.Utils.QuickCheck |
| Codata | Agda.Syntax.Concrete.Definitions |
| code | Agda.Syntax.Parser.Lexer |
| CoinductionKit | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.Builtin.Coinduction |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.Builtin.Coinduction |
| coinductionKit | Agda.TypeChecking.Rules.Builtin.Coinduction |
| CoInductive | Agda.Syntax.Common |
| CoinductiveDatatype | Agda.TypeChecking.Coverage |
| col | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| coldescr | Agda.Utils.Warshall |
| collect | Agda.Utils.QuickCheck |
| colon | Agda.Utils.Pretty |
| cols | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| Column | Agda.Termination.Lexicographic |
| columns | Agda.Termination.Lexicographic |
| comma | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Command | Agda.Interaction.CommandLine.CommandLine |
| command | Agda.Interaction.GhciTop |
| CommandLineOptions | Agda.Interaction.Options |
| commandLineOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Comment | |
| 1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| commutative | Agda.Utils.TestHelpers |
| commuteM | Agda.Utils.Monad |
| comp' | Agda.Auto.Typecheck |
| compactP | Agda.Utils.Permutation |
| compareArgs | Agda.TypeChecking.Conversion |
| compareAtom | Agda.TypeChecking.Conversion |
| compareLevel | Agda.TypeChecking.UniversePolymorphism |
| compareSizes | Agda.TypeChecking.SizedTypes |
| compareSort | Agda.TypeChecking.Conversion |
| compareTel | Agda.TypeChecking.Conversion |
| compareTerm | Agda.TypeChecking.Conversion |
| compareType | Agda.TypeChecking.Conversion |
| Comparison | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CompilationError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Compile | Agda.Compiler.Epic.CompileState |
| compile | |
| 1 (Function) | Agda.TypeChecking.CompiledClause |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| compileClauses | |
| 1 (Function) | Agda.TypeChecking.CompiledClause |
| 2 (Function) | Agda.Compiler.Epic.FromAgda |
| CompiledClauses | Agda.TypeChecking.CompiledClause |
| CompiledDataPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledEpicPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compileDir | Agda.Compiler.MAlonzo.Compiler |
| CompiledPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| CompiledTypePragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| compilerMain | |
| 1 (Function) | Agda.Compiler.Epic.Compiler |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| CompileState | |
| 1 (Type/Class) | Agda.Compiler.Epic.CompileState |
| 2 (Data Constructor) | Agda.Compiler.Epic.CompileState |
| complete | Agda.Termination.CallGraph |
| composeP | Agda.Utils.Permutation |
| composePol | Agda.TypeChecking.Polarity |
| compress | Agda.Interaction.Highlighting.Precise |
| CompressedFile | Agda.Interaction.Highlighting.Precise |
| computeEdge | Agda.TypeChecking.Positivity |
| computeNeighbourhood | Agda.TypeChecking.Coverage |
| ComputeOccurrences | Agda.TypeChecking.Positivity |
| computeOccurrences | Agda.TypeChecking.Positivity |
| computePolarity | Agda.TypeChecking.Polarity |
| computeSizeConstraint | Agda.TypeChecking.SizedTypes |
| Con | |
| 1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| conAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ConArgType | Agda.TypeChecking.Positivity |
| conBranches | Agda.TypeChecking.CompiledClause |
| conCase | Agda.TypeChecking.CompiledClause |
| concatargs | Agda.Auto.CaseSplit |
| concatMapM | Agda.Utils.Monad |
| concatOccurs | Agda.TypeChecking.Positivity |
| ConcreteDef | Agda.Syntax.Common |
| ConcreteMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| concreteToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| concreteToAbstract_ | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| conData | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| condecl | Agda.Compiler.MAlonzo.Compiler |
| conFreq | Agda.TypeChecking.Test.Generators |
| ConHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conhqn | Agda.Compiler.MAlonzo.Misc |
| conHsCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conInd | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| conjoin | Agda.Utils.QuickCheck |
| ConMP | Agda.TypeChecking.Coverage.Match |
| ConName | |
| 1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| ConnectHandle | Agda.Auto.NarrowingSearch |
| ConP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| conPars | |
| 1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Compiler.Epic.CompileState |
| ConPos | Agda.TypeChecking.With |
| Cons | Agda.Interaction.GhciTop |
| conSrcCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Const | Agda.Auto.Syntax |
| ConstDef | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| Constr | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| Constraint | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.Utils.Warshall |
| ConstraintClosure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Constraints | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.Utils.Warshall |
| ConstRef | Agda.Auto.Syntax |
| constrIrr | Agda.Compiler.Epic.ConstructorIrrelevancy |
| constrType | Agda.Compiler.Epic.Forcing |
| Constructor | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 5 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| constructorArity | |
| 1 (Function) | Agda.Compiler.Epic.CompileState |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| constructorForm | Agda.TypeChecking.Primitive |
| constructorImpossible | Agda.Auto.Typecheck |
| ConstructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| constructorMismatch | Agda.TypeChecking.Rules.LHS.Unify |
| ConstructorName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| ConstructorPatternInWrongDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| constructorsInClause | Agda.TypeChecking.With |
| constructorsInClauses | Agda.TypeChecking.With |
| constructPats | Agda.Auto.Convert |
| constructs | Agda.TypeChecking.Rules.Data |
| Cont | Agda.Utils.Monad |
| containsAbsurdPattern | Agda.TypeChecking.Rules.Def |
| contains_constructor | Agda.Auto.Convert |
| Context | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ContextEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| contextOfMeta | Agda.Interaction.BasicOps |
| Continue | Agda.Interaction.CommandLine.CommandLine |
| continueAfter | Agda.Interaction.CommandLine.CommandLine |
| ContinueIn | Agda.Interaction.CommandLine.CommandLine |
| continuous | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| continuousPerLine | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Contravariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| convertLineEndings | Agda.Utils.Unicode |
| copyarg | Agda.Auto.Typecheck |
| copyScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| costAbsurdLam | Agda.Auto.SearchControl |
| costAddVarDepth | Agda.Auto.CaseSplit |
| costAppConstructor | Agda.Auto.SearchControl |
| costAppConstructorSingle | Agda.Auto.SearchControl |
| costAppExtraRef | Agda.Auto.SearchControl |
| costAppHint | Agda.Auto.SearchControl |
| costAppHintUsed | Agda.Auto.SearchControl |
| costAppRecCall | Agda.Auto.SearchControl |
| costAppRecCallUsed | Agda.Auto.SearchControl |
| costAppVar | Agda.Auto.SearchControl |
| costAppVarUsed | Agda.Auto.SearchControl |
| costCaseSplitHigh | Agda.Auto.CaseSplit |
| costCaseSplitLow | Agda.Auto.CaseSplit |
| costCaseSplitVeryHigh | Agda.Auto.CaseSplit |
| costEqCong | Agda.Auto.SearchControl |
| costEqEnd | Agda.Auto.SearchControl |
| costEqStep | Agda.Auto.SearchControl |
| costEqSym | Agda.Auto.SearchControl |
| costIncrease | Agda.Auto.SearchControl |
| costInferredTypeUnkown | Agda.Auto.SearchControl |
| costIotaStep | Agda.Auto.SearchControl |
| costLam | Agda.Auto.SearchControl |
| costLamUnfold | Agda.Auto.SearchControl |
| costPi | Agda.Auto.SearchControl |
| costSort | Agda.Auto.SearchControl |
| costUnification | Agda.Auto.SearchControl |
| costUnificationOccurs | Agda.Auto.SearchControl |
| count | Agda.Utils.ReadP |
| Covariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| cover | |
| 1 (Function) | Agda.Utils.QuickCheck |
| 2 (Function) | Agda.TypeChecking.Coverage |
| CoverageCantSplitOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageCantSplitType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CoverageFailure | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Covering | Agda.TypeChecking.Coverage |
| CoverM | Agda.TypeChecking.Coverage |
| createInterface | Agda.Interaction.Imports |
| createMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| createModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| CSAbsurd | Agda.Auto.CaseSplit |
| CSCtx | Agda.Auto.CaseSplit |
| CSOmittedArg | Agda.Auto.CaseSplit |
| CSPat | Agda.Auto.CaseSplit |
| CSPatConApp | Agda.Auto.CaseSplit |
| CSPatExp | Agda.Auto.CaseSplit |
| CSPatI | Agda.Auto.CaseSplit |
| CSPatVar | Agda.Auto.CaseSplit |
| CSWith | Agda.Auto.CaseSplit |
| cthandles | Agda.Auto.NarrowingSearch |
| ctparent | Agda.Auto.NarrowingSearch |
| ctpriometa | Agda.Auto.NarrowingSearch |
| CTree | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| ctsub | Agda.Auto.NarrowingSearch |
| Ctx | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ctxEntry | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| CtxId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ctxId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| curDefs | Agda.Compiler.MAlonzo.Misc |
| curHsMod | Agda.Compiler.MAlonzo.Misc |
| curIF | Agda.Compiler.MAlonzo.Misc |
| curMName | Agda.Compiler.MAlonzo.Misc |
| CurrentDir | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| CurrentInput | Agda.Syntax.Parser.Alex |
| currentModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| currentMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| curSig | Agda.Compiler.MAlonzo.Misc |
| CyclicModuleDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Data | Agda.Syntax.Concrete |
| dataAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataCons | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataDecls | Agda.Compiler.Epic.CompileState |
| DataDef | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| dataHsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataInduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DataInfo | Agda.TypeChecking.Datatypes |
| dataIxs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DataMustEndInSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataOrRecordType | Agda.TypeChecking.Rules.LHS.Unify |
| dataParameters | Agda.Compiler.Epic.Forcing |
| dataPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dataSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Datatype | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DatatypeInfo | Agda.TypeChecking.Datatypes |
| datatypeIxs | Agda.TypeChecking.Datatypes |
| datatypeIxTel | Agda.TypeChecking.Datatypes |
| datatypeName | Agda.TypeChecking.Datatypes |
| datatypePars | Agda.TypeChecking.Datatypes |
| datatypeParTel | Agda.TypeChecking.Datatypes |
| deBruijnIndex | Agda.Interaction.MakeCase |
| DeBruijnPat | Agda.Termination.TermCheck |
| debug | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad |
| decDigit | Agda.Utils.Char |
| Declaration | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| DeclarationException | Agda.Syntax.Concrete.Definitions |
| DeclarationPanic | Agda.Syntax.Concrete.Definitions |
| DeclCont | Agda.Auto.Syntax |
| DeclInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| declName | Agda.Syntax.Info |
| declRange | Agda.Syntax.Info |
| declsForPrim | Agda.Compiler.MAlonzo.Primitives |
| decode | Agda.TypeChecking.Serialise |
| DecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| decodeFile | Agda.TypeChecking.Serialise |
| decompress | Agda.Interaction.Highlighting.Precise |
| decr | Agda.Termination.CallGraph |
| decrConf | Agda.TypeChecking.Test.Generators |
| decreasing | Agda.Termination.CallGraph |
| Def | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| defAbstract | |
| 1 (Function) | Agda.Syntax.Info |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defAccess | Agda.Syntax.Info |
| DefArg | Agda.TypeChecking.Positivity |
| Default | Agda.Compiler.Epic.AuxAST |
| defaultArg | Agda.Syntax.Common |
| defaultDisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defaultFixity | Agda.Syntax.Fixity |
| defaultFixity' | Agda.Syntax.Fixity |
| defaultFrequencies | Agda.TypeChecking.Test.Generators |
| defaultImportDir | Agda.Syntax.Concrete |
| defaultNotation | Agda.Syntax.Notation |
| defaultOptions | Agda.Interaction.Options |
| defaultParseFlags | Agda.Syntax.Parser.Monad |
| defaultVerbosity | Agda.Interaction.Options |
| defClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defDelayed | |
| 1 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Compiler.Epic.CompileState |
| defDisplay | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defFixity | Agda.Syntax.Info |
| defFreq | Agda.TypeChecking.Test.Generators |
| DefinedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| DefInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| defInfo | Agda.Syntax.Info |
| Definition | |
| 1 (Type/Class) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| definition | Agda.Compiler.MAlonzo.Compiler |
| DefinitionIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Definitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| definitions | |
| 1 (Function) | Agda.Compiler.Epic.CompileState |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| definitionSite | Agda.Interaction.Highlighting.Precise |
| defIsRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Defn | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DefName | |
| 1 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| defName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DefNode | Agda.TypeChecking.Positivity |
| DefP | Agda.Syntax.Abstract |
| defRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| defType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Delayed | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Dependent | Agda.Interaction.GhciTop |
| depthofvar | Agda.Auto.CaseSplit |
| deref | Agda.Utils.Pointer |
| detecteliminand | Agda.Auto.Syntax |
| detectsemiflex | Agda.Auto.Syntax |
| diagonal | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| DifferentArities | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| disableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| disjoin | Agda.Utils.QuickCheck |
| Display | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| displayErrorAndExit | Agda.Interaction.GhciTop |
| DisplayForm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| displayForm | Agda.TypeChecking.DisplayForm |
| displayFormsEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| displayStatus | Agda.Interaction.GhciTop |
| DisplayTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| display_info | Agda.Interaction.GhciTop |
| display_info' | Agda.Interaction.GhciTop |
| display_infoD | Agda.Interaction.GhciTop |
| Dist | Agda.Utils.Warshall |
| Distance | Agda.Utils.Warshall |
| distinct | Agda.Utils.List |
| divConf | Agda.TypeChecking.Test.Generators |
| DLub | Agda.Syntax.Internal |
| dLub | Agda.TypeChecking.Substitute |
| Doc | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Type/Class) | Agda.TypeChecking.Pretty |
| doclos | Agda.Auto.Syntax |
| DoesNotConstructAnElementOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| doEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DomainFree | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| DomainFull | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| Done | Agda.TypeChecking.CompiledClause |
| DontCare | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| dontCare | Agda.Auto.Syntax |
| dontEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DontExpandLast | Agda.TypeChecking.Rules.Term |
| DontKnow | |
| 1 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| 2 (Data Constructor) | Agda.Compiler.Epic.Erasure |
| 3 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Unify |
| DontOpen | Agda.Syntax.Concrete |
| dontReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| DontTouchMe | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| DoOpen | Agda.Syntax.Concrete |
| Dot | Agda.Syntax.Concrete |
| DotP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| DotPatternCtx | Agda.Syntax.Fixity |
| DotPatternInst | Agda.TypeChecking.Rules.LHS |
| dotPatternInsts | Agda.TypeChecking.Rules.LHS |
| DottedPattern | Agda.Interaction.Highlighting.Precise |
| DotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| dotVars | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| double | Agda.Utils.Pretty |
| doubleblock | Agda.Auto.NarrowingSearch |
| doubleQuotes | Agda.Utils.Pretty |
| DPI | Agda.TypeChecking.Rules.LHS |
| dropDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| drophid | Agda.Auto.CaseSplit |
| dropI | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| dryInstantiate | Agda.Auto.NarrowingSearch |
| dsubname | Agda.Compiler.MAlonzo.Misc |
| DTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| dummy | Agda.Compiler.MAlonzo.Misc |
| DuplicateBuiltinBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateConstructors | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DuplicateImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| DWithApp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| eatNextChar | Agda.Syntax.Parser.LookAhead |
| Edge | |
| 1 (Type/Class) | Agda.TypeChecking.Positivity |
| 2 (Data Constructor) | Agda.TypeChecking.Positivity |
| edges | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Warshall |
| EE | Agda.Auto.Syntax |
| EitherOrBoth | Agda.Utils.Map |
| El | Agda.Syntax.Internal |
| el | Agda.TypeChecking.Primitive |
| elements | Agda.Utils.QuickCheck |
| Ellipsis | Agda.Syntax.Concrete |
| Elr | Agda.Auto.Syntax |
| EmbPrj | Agda.TypeChecking.Serialise |
| empty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Utils.Graph |
| 3 (Function) | Agda.Utils.Trie |
| 4 (Function) | Agda.Termination.CallGraph |
| 5 (Function) | Agda.TypeChecking.Pretty |
| emptyConstraints | Agda.Utils.Warshall |
| emptyLayout | Agda.Syntax.Parser.Layout |
| emptyNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| emptyScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| emptyScopeInfo | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| emptySignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| emptySolution | Agda.Utils.Warshall |
| EmptyTel | Agda.Syntax.Internal |
| emptyUState | Agda.TypeChecking.Rules.LHS.Unify |
| empty_layout | Agda.Syntax.Parser.Lexer |
| enableDisplayForms | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| encode | Agda.TypeChecking.Serialise |
| encodeFile | Agda.TypeChecking.Serialise |
| encodeModuleName | Agda.Compiler.MAlonzo.Encode |
| end | Agda.Syntax.Parser.LexActions |
| endBy | Agda.Utils.ReadP |
| endBy1 | Agda.Utils.ReadP |
| endWith | Agda.Syntax.Parser.LexActions |
| end_ | Agda.Syntax.Parser.LexActions |
| ensureFileLoaded | Agda.Interaction.GhciTop |
| enterClosure | Agda.TypeChecking.Monad.Closure, Agda.TypeChecking.Monad |
| Env | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| envAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envAnonymousModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envContext | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envDisplayFormsEnabled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envEtaContractImplicit | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envImportPath | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envLetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envMutualBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envRange | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envReifyInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| envReplace | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| eof | Agda.Syntax.Parser.LexActions |
| Epic | Agda.Interaction.GhciTop |
| EpicCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| epicError | Agda.Compiler.Epic.CompileState |
| EpicFun | Agda.Compiler.Epic.AuxAST |
| eqelr | Agda.Auto.CaseSplit |
| eqrcBegin | Agda.Auto.Syntax |
| eqrcCong | Agda.Auto.Syntax |
| eqrcEnd | Agda.Auto.Syntax |
| eqrcId | Agda.Auto.Syntax |
| eqrcStep | Agda.Auto.Syntax |
| eqrcSym | Agda.Auto.Syntax |
| EqReasoningConsts | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Auto.Syntax |
| EqReasoningState | Agda.Auto.Syntax |
| EqRSChain | Agda.Auto.Syntax |
| EqRSNone | Agda.Auto.Syntax |
| EqRSPrf1 | Agda.Auto.Syntax |
| EqRSPrf2 | Agda.Auto.Syntax |
| EqRSPrf3 | Agda.Auto.Syntax |
| Equal | Agda.TypeChecking.Rules.LHS.Unify |
| equalArgs | Agda.TypeChecking.Conversion |
| equalAtom | Agda.TypeChecking.Conversion |
| Equality | Agda.TypeChecking.Rules.LHS.Unify |
| equalLevel | Agda.TypeChecking.Conversion |
| equals | Agda.Utils.Pretty |
| equalSort | Agda.TypeChecking.Conversion |
| equalTerm | Agda.TypeChecking.Conversion |
| equalType | Agda.TypeChecking.Conversion |
| Erasure | Agda.Compiler.Epic.Erasure |
| erasure | Agda.Compiler.Epic.Erasure |
| ErasureState | |
| 1 (Type/Class) | Agda.Compiler.Epic.Erasure |
| 2 (Data Constructor) | Agda.Compiler.Epic.Erasure |
| eriEqRState | Agda.Auto.SearchControl |
| eriInfTypeUnknown | Agda.Auto.SearchControl |
| eriIotaStep | Agda.Auto.SearchControl |
| eriIsEliminand | Agda.Auto.SearchControl |
| eriMain | Agda.Auto.SearchControl |
| eriPickSubsVar | Agda.Auto.SearchControl |
| eriUnifs | Agda.Auto.SearchControl |
| eriUsedVars | Agda.Auto.SearchControl |
| errError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| errHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| errInput | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| errMsg | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| Error | |
| 1 (Data Constructor) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| errorTitle | Agda.Interaction.GhciTop |
| errPos | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| errPrevToken | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| escape | Agda.Interaction.Highlighting.Vim |
| escapeContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| etaContract | Agda.TypeChecking.EtaContract |
| etaContractBody | Agda.Auto.Convert |
| etaContractRecord | Agda.TypeChecking.Records |
| etaExpandBlocked | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| etaExpandClause | Agda.TypeChecking.Positivity |
| etaExpandListeners | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| etaExpandMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| etaExpandMetaSafe | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| etaExpandRecord | Agda.TypeChecking.Records |
| etaOnce | Agda.TypeChecking.EtaContract |
| EtaPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| ETel | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| evalIn | Agda.Interaction.CommandLine.CommandLine |
| evalInCurrent | Agda.Interaction.BasicOps |
| evalInMeta | Agda.Interaction.BasicOps |
| evalTerm | Agda.Interaction.CommandLine.CommandLine |
| everythingBut | Agda.Utils.Generics |
| everythingInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| everywhereBut' | Agda.Utils.Generics |
| everywhereButM' | Agda.Utils.Generics |
| Exception | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ExceptionT | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Exception |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Exception |
| ExitCode | Agda.Interaction.CommandLine.CommandLine |
| Exp | Agda.Auto.Syntax |
| expandbind | Agda.Auto.NarrowingSearch |
| expandExp | Agda.Auto.Syntax |
| ExpandHidden | Agda.TypeChecking.Rules.Term |
| ExpandLast | Agda.TypeChecking.Rules.Term |
| expandLitPattern | Agda.TypeChecking.Rules.LHS.Split |
| expandP | Agda.Utils.Permutation |
| expectFailure | Agda.Utils.QuickCheck |
| exportedNamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Expr | |
| 1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| ExpRefInfo | |
| 1 (Type/Class) | Agda.Auto.SearchControl |
| 2 (Data Constructor) | Agda.Auto.SearchControl |
| ExprHole | Agda.Syntax.Notation |
| ExprInfo | Agda.Syntax.Info |
| exprInfo | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| exprParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ExprRange | Agda.Syntax.Info |
| ExprSource | Agda.Syntax.Info |
| ExprView | Agda.Syntax.Concrete.Operators.Parser |
| exprView | Agda.Syntax.Concrete.Operators.Parser |
| extendConf | Agda.TypeChecking.Test.Generators |
| extendSolution | Agda.Utils.Warshall |
| ExtendTel | Agda.Syntax.Internal |
| extendWithTelConf | Agda.TypeChecking.Test.Generators |
| extractblkinfos | Agda.Auto.NarrowingSearch |
| extractNthElement | Agda.Utils.List |
| extractNthElement' | Agda.Utils.List |
| extraref | Agda.Auto.SearchControl |
| Fail | Agda.TypeChecking.CompiledClause |
| Failed | Agda.Auto.NarrowingSearch |
| failOnException | Agda.Interaction.Exceptions, Agda.Interaction.GhciTop |
| Failure | Agda.Utils.QuickCheck |
| fakeD | Agda.Compiler.MAlonzo.Misc |
| fakeDQ | Agda.Compiler.MAlonzo.Misc |
| fakeDS | Agda.Compiler.MAlonzo.Misc |
| fakeExp | Agda.Compiler.MAlonzo.Misc |
| fakeType | Agda.Compiler.MAlonzo.Misc |
| fastDistinct | Agda.Utils.List |
| fcat | Agda.Utils.Pretty |
| fCtx | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Field | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| FieldOutsideRecord | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Fields | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| File | Agda.Interaction.Highlighting.Precise |
| FileNotFound | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| filePath | Agda.Utils.FileName |
| filterKeys | Agda.Utils.Map |
| filterScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| finally | Agda.Utils.Monad |
| findClause | Agda.Interaction.MakeCase |
| findClauseDeep | Agda.Auto.Convert |
| FindError | Agda.Interaction.FindFile |
| findErrorToTypeError | Agda.Interaction.FindFile |
| findFile | Agda.Interaction.FindFile |
| findFile' | Agda.Interaction.FindFile |
| findFile'' | Agda.Interaction.FindFile |
| findIdx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| findInterfaceFile | Agda.Interaction.FindFile |
| findMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| findPath | Agda.Utils.Graph |
| findperm | Agda.Auto.CaseSplit |
| findPosition | Agda.Compiler.Epic.Forcing |
| Finite | Agda.Utils.Warshall |
| fInteger | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| fInteraction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| firstPart | Agda.TypeChecking.Telescope |
| fitsIn | Agda.TypeChecking.Rules.Data |
| Fixed | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| Fixity | Agda.Syntax.Fixity |
| Fixity' | |
| 1 (Type/Class) | Agda.Syntax.Fixity |
| 2 (Data Constructor) | Agda.Syntax.Fixity |
| fixityLevel | Agda.Syntax.Fixity |
| fixSize | Agda.TypeChecking.Test.Generators |
| fixSizeConf | Agda.TypeChecking.Test.Generators |
| Flag | Agda.Interaction.Options |
| flattenSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
| flattenTel | Agda.TypeChecking.Telescope |
| Flex | |
| 1 (Data Constructor) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| flexiblePatterns | Agda.TypeChecking.Rules.LHS |
| flexibleVariables | Agda.TypeChecking.SizedTypes |
| FlexibleVars | Agda.TypeChecking.Rules.LHS.Problem |
| flexibleVars | Agda.TypeChecking.Free |
| FlexId | Agda.Utils.Warshall |
| flexScope | Agda.Utils.Warshall |
| float | Agda.Utils.Pretty |
| fmapM | Agda.Utils.Monad |
| fMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| fmExp | Agda.Auto.Convert |
| fmExps | Agda.Auto.Convert |
| FMode | Agda.Auto.Syntax |
| fmType | Agda.Auto.Convert |
| fMutual | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| fName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Focus | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| focusCon | Agda.TypeChecking.Rules.LHS.Problem |
| focusConArgs | Agda.TypeChecking.Rules.LHS.Problem |
| focusDatatype | Agda.TypeChecking.Rules.LHS.Problem |
| focusHoleIx | Agda.TypeChecking.Rules.LHS.Problem |
| focusIndices | Agda.TypeChecking.Rules.LHS.Problem |
| focusOutPat | Agda.TypeChecking.Rules.LHS.Problem |
| focusParams | Agda.TypeChecking.Rules.LHS.Problem |
| focusRange | Agda.TypeChecking.Rules.LHS.Problem |
| focusType | Agda.TypeChecking.Rules.LHS.Problem |
| foldM' | Agda.Compiler.Epic.Forcing |
| FoldState | |
| 1 (Type/Class) | Agda.Compiler.Epic.Forcing |
| 2 (Data Constructor) | Agda.Compiler.Epic.Forcing |
| foldTerm | Agda.Syntax.Internal.Generic |
| followedBy | Agda.Syntax.Parser.LexActions |
| forAll | Agda.Utils.QuickCheck |
| forAllShrink | Agda.Utils.QuickCheck |
| force | |
| 1 (Function) | Agda.Syntax.Strict |
| 2 (Function) | Agda.TypeChecking.Forcing |
| Forced | Agda.Syntax.Common |
| forceData | Agda.TypeChecking.Rules.Data |
| forcedVariables | Agda.TypeChecking.Forcing |
| forceM | Agda.Utils.Monad |
| forcePi | Agda.TypeChecking.Rules.Term |
| forgetM | Agda.Utils.Monad |
| Free | Agda.TypeChecking.Free |
| freeIn | |
| 1 (Function) | Agda.TypeChecking.Free |
| 2 (Function) | Agda.Auto.Convert |
| freeInIgnoringSorts | Agda.TypeChecking.Free |
| FreeVars | Agda.TypeChecking.Free |
| freeVars | Agda.TypeChecking.Free |
| freevars | Agda.Auto.CaseSplit |
| freeVarsToApply | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| Freqs | Agda.TypeChecking.Test.Generators |
| Frequencies | Agda.TypeChecking.Test.Generators |
| frequency | Agda.Utils.QuickCheck |
| Fresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| fresh | Agda.Utils.Fresh |
| freshAbstractName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| freshAbstractName_ | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| freshAbstractQName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| freshName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| freshName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| freshNoName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| freshNoName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| FreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| from | Agda.Interaction.Highlighting.Range |
| fromAgda | Agda.Compiler.Epic.FromAgda |
| fromDiagonals | Agda.Termination.Lexicographic |
| fromIndexList | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| fromJust | Agda.Utils.Maybe |
| fromList | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Termination.CallGraph |
| fromLists | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| fromLiteral | Agda.TypeChecking.Primitive |
| fromMaybe | Agda.Utils.Maybe |
| fromMaybeM | Agda.Utils.Maybe |
| frommy | Agda.Auto.Convert |
| frommyClause | Agda.Auto.Convert |
| frommyExp | Agda.Auto.Convert |
| frommyExps | Agda.Auto.Convert |
| frommyType | Agda.Auto.Convert |
| fromReducedTerm | Agda.TypeChecking.Primitive |
| FromTerm | Agda.TypeChecking.Primitive |
| fromTerm | Agda.TypeChecking.Primitive |
| FromTermFunction | Agda.TypeChecking.Primitive |
| fsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| fullRender | Agda.Utils.Pretty |
| Fun | |
| 1 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| 6 (Type/Class) | Agda.TypeChecking.Primitive |
| funAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funArgs | Agda.Compiler.Epic.AuxAST |
| FunClause | Agda.Syntax.Concrete |
| funClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funComment | Agda.Compiler.Epic.AuxAST |
| funCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Function | |
| 1 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| FunctionCtx | Agda.Syntax.Fixity |
| FunctionInverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| functionInverse | Agda.TypeChecking.Injectivity |
| FunctionSpaceDomainCtx | Agda.Syntax.Fixity |
| FunDef | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| funDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funEpicCode | Agda.Compiler.Epic.AuxAST |
| funExpr | Agda.Compiler.Epic.AuxAST |
| funFreq | Agda.TypeChecking.Test.Generators |
| funInline | Agda.Compiler.Epic.AuxAST |
| funInv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funName | Agda.Compiler.Epic.AuxAST |
| funPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| funs | Agda.Compiler.Epic.Erasure |
| FunV | Agda.Syntax.Internal |
| FunView | Agda.Syntax.Internal |
| funView | Agda.Syntax.Internal |
| fuseRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| fuseRanges | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| FV | Agda.TypeChecking.Free |
| fv | Agda.Compiler.Epic.AuxAST |
| FVs | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| fwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| gApply | Agda.TypeChecking.Primitive |
| gather | Agda.Utils.ReadP |
| GaveUp | Agda.Utils.QuickCheck |
| Gen | Agda.Utils.QuickCheck |
| genArgs | Agda.TypeChecking.Test.Generators |
| GenC | Agda.TypeChecking.Test.Generators |
| genC | Agda.TypeChecking.Test.Generators |
| genConf | Agda.TypeChecking.Test.Generators |
| generateErrorInfo | Agda.Interaction.Highlighting.Generate |
| generateHTML | Agda.Interaction.Highlighting.HTML |
| generateSyntaxInfo | Agda.Interaction.Highlighting.Generate |
| generateVimFile | Agda.Interaction.Highlighting.Vim |
| genericElemIndex | Agda.Utils.List |
| GenericError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| GenericSplitError | Agda.TypeChecking.Coverage |
| GenericUnifyException | Agda.TypeChecking.Rules.LHS.Unify |
| genGraph | Agda.Utils.Warshall |
| genGraph_ | Agda.Utils.Warshall |
| GenPart | Agda.Syntax.Notation |
| genPath | Agda.Utils.Warshall |
| get | Agda.Utils.ReadP |
| getAllArgs | Agda.Auto.Typecheck |
| getAnonymousVariables | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| getArgOccurrence | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getArity | Agda.TypeChecking.Polarity |
| getblks | Agda.Auto.CaseSplit |
| getBuiltin | Agda.TypeChecking.Monad.Builtin |
| getBuiltin' | Agda.TypeChecking.Monad.Builtin |
| getBuiltins | Agda.Compiler.Epic.Primitive |
| getBuiltinThings | Agda.TypeChecking.Monad.Builtin |
| getConPar | Agda.Compiler.Epic.CompileState |
| getConst | Agda.Auto.Convert |
| getConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getConstraint | Agda.Interaction.BasicOps |
| getConstraints | |
| 1 (Function) | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Interaction.BasicOps |
| getConstrTag | Agda.Compiler.Epic.CompileState |
| getConstructorData | Agda.TypeChecking.Datatypes |
| getContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getContextArgs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getContextId | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getContextTelescope | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getContextTerms | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getCurrentFile | Agda.Interaction.GhciTop |
| getCurrentModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| getCurrentScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getDatatype | Agda.Auto.Typecheck |
| getDatatypeInfo | Agda.TypeChecking.Datatypes |
| getDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| getDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| getDefFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getDelayed | Agda.Compiler.Epic.CompileState |
| getdfv | Agda.Auto.Convert |
| getEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| getEqs | Agda.Auto.Convert |
| getFixity | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getHaskellImports | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| getHsType | Agda.Compiler.HaskellTypes |
| getHsVar | Agda.Compiler.HaskellTypes |
| getImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| getImports | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| getIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| getinfo | Agda.Auto.SearchControl |
| getInput | Agda.Syntax.Parser.LookAhead |
| getInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| getInstantiatedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getInteractionMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getInteractionRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getInteractionScope | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getInterface | Agda.Interaction.Imports |
| getInterface' | Agda.Interaction.Imports |
| getIrrFilter | Agda.Compiler.Epic.CompileState |
| getLexInput | Agda.Syntax.Parser.Alex |
| getLexState | Agda.Syntax.Parser.Monad |
| getLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getMain | Agda.Compiler.Epic.CompileState |
| getMeta | Agda.Auto.Convert |
| getMetaEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| getMetaInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| getMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getMetaPriority | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getMetaRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getMetaScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| getMetaSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| getMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getModuleFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getMutualBlocks | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| getNamedScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| getNArgs | Agda.Auto.Typecheck |
| getNatish | Agda.Compiler.Epic.NatDetection |
| getOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
| getOpenMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| getParseFlags | Agda.Syntax.Parser.Monad |
| getParseInterval | Agda.Syntax.Parser.Monad |
| getPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getPolarity' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getPrimitive | Agda.TypeChecking.Monad.Builtin |
| getRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| getRanges | Agda.Interaction.Highlighting.Range |
| getRangesA | Agda.Interaction.Highlighting.Range |
| getRecordConstructor | Agda.TypeChecking.Records |
| getRecordConstructorType | Agda.TypeChecking.Records |
| getRecordDef | Agda.TypeChecking.Records |
| getRecordFieldNames | Agda.TypeChecking.Records |
| getRecordFieldTypes | Agda.TypeChecking.Records |
| getScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| getSecFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| getSizeConstraints | Agda.TypeChecking.SizedTypes |
| getSizeMetas | Agda.TypeChecking.SizedTypes |
| getSolvedInteractionPoints | Agda.Interaction.BasicOps |
| getSort | Agda.Syntax.Internal |
| getStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad |
| getSub | Agda.TypeChecking.Rules.LHS.Unify |
| getVarInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| getVerbosity | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| getVisitedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| getVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| give | Agda.Interaction.BasicOps |
| giveExpr | Agda.Interaction.BasicOps |
| giveMeta | Agda.Interaction.CommandLine.CommandLine |
| give_gen | Agda.Interaction.GhciTop |
| give_gen' | Agda.Interaction.GhciTop |
| GM | Agda.Utils.Warshall |
| GoalCommand | Agda.Interaction.GhciTop |
| goal_command | Agda.Interaction.GhciTop |
| gpi | Agda.TypeChecking.Primitive |
| Graph | |
| 1 (Type/Class) | Agda.Utils.Graph |
| 2 (Data Constructor) | Agda.Utils.Graph |
| 3 (Type/Class) | Agda.Utils.Warshall |
| 4 (Data Constructor) | Agda.Utils.Warshall |
| graph | Agda.Utils.Warshall |
| groupBy' | Agda.Utils.List |
| groupOn | Agda.Utils.List |
| growGraph | Agda.Utils.Graph |
| growingElements | Agda.Utils.QuickCheck |
| gshow' | Agda.Compiler.MAlonzo.Misc |
| Guard | Agda.Interaction.BasicOps |
| guardConstraint | Agda.TypeChecking.Constraints |
| Guarded | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| handleAbort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| handleParseException | Agda.Interaction.Exceptions, Agda.Interaction.GhciTop |
| HandleSol | Agda.Auto.NarrowingSearch |
| hang | Agda.Utils.Pretty |
| hasBadRigid | Agda.TypeChecking.MetaVars.Occurs |
| hasCompiledData | Agda.Compiler.MAlonzo.Primitives |
| HasFresh | Agda.Utils.Fresh |
| hash | Agda.Utils.Hash |
| hasInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| HaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellKind | Agda.Compiler.HaskellTypes |
| haskellKind | Agda.Compiler.HaskellTypes |
| HaskellRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| haskellType | Agda.Compiler.HaskellTypes |
| HasMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| HasPolarity | Agda.TypeChecking.Polarity |
| HasRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| HasType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| hasVerbosity | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| HasZero | Agda.Termination.Semiring |
| haveSizedTypes | Agda.TypeChecking.SizedTypes |
| hcat | Agda.Utils.Pretty |
| Head | Agda.Syntax.Abstract.Views |
| HeadCon | Agda.Syntax.Abstract.Views |
| HeadDef | Agda.Syntax.Abstract.Views |
| HeadNormal | Agda.Interaction.BasicOps |
| headSymbol | Agda.TypeChecking.Injectivity |
| headToExpr | Agda.Syntax.Abstract.Views |
| HeadVar | Agda.Syntax.Abstract.Views |
| help | Agda.Interaction.CommandLine.CommandLine |
| hequalMetavar | Agda.Auto.NarrowingSearch |
| Here | |
| 1 (Data Constructor) | Agda.TypeChecking.Positivity |
| 2 (Data Constructor) | Agda.TypeChecking.With |
| here | Agda.TypeChecking.Positivity |
| hexDigit | Agda.Utils.Char |
| hGetContents | Agda.Utils.IO.Locale |
| HI | |
| 1 (Type/Class) | Agda.Auto.CaseSplit |
| 2 (Data Constructor) | Agda.Auto.CaseSplit |
| Hidden | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Common |
| HiddenArg | Agda.Syntax.Concrete |
| hiddenArgumentCtx | Agda.Syntax.Fixity |
| HiddenArgV | Agda.Syntax.Concrete.Operators.Parser |
| hiddenFreq | Agda.TypeChecking.Test.Generators |
| HiddenFreqs | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| hiddenFreqs | Agda.TypeChecking.Test.Generators |
| HiddenP | Agda.Syntax.Concrete |
| hide | Agda.Syntax.Common |
| Hiding | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| HighlightingInfo | Agda.Interaction.Highlighting.Precise |
| highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HintMode | Agda.Auto.Syntax |
| HMNormal | Agda.Auto.Syntax |
| HMRecCall | Agda.Auto.Syntax |
| HNALConPar | Agda.Auto.Syntax |
| HNALCons | Agda.Auto.Syntax |
| HNALNil | Agda.Auto.Syntax |
| HNApp | Agda.Auto.Syntax |
| HNArgList | Agda.Auto.Syntax |
| hnarglist | Agda.Auto.Typecheck |
| hnb | Agda.Auto.Typecheck |
| hnc | Agda.Auto.Typecheck |
| HNDone | Agda.Auto.Typecheck |
| HNExp | Agda.Auto.Syntax |
| HNLam | Agda.Auto.Syntax |
| HNMeta | Agda.Auto.Typecheck |
| hnn | Agda.Auto.Typecheck |
| hnn' | Agda.Auto.Typecheck |
| HNNBlks | Agda.Auto.Typecheck |
| hnn_blks | Agda.Auto.Typecheck |
| hnn_checkstep | Agda.Auto.Typecheck |
| HNPi | Agda.Auto.Syntax |
| HNRes | Agda.Auto.Typecheck |
| HNSort | Agda.Auto.Syntax |
| Hole | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal.Pattern |
| hole | Agda.Syntax.Parser.Comments |
| HoleName | Agda.Syntax.Notation |
| holeName | Agda.Syntax.Notation |
| holes | Agda.Utils.List |
| holeTarget | Agda.Syntax.Notation |
| hPi | Agda.TypeChecking.Primitive |
| hsApp | Agda.Compiler.HaskellTypes |
| hsCast | Agda.Compiler.MAlonzo.Compiler |
| hsCast' | Agda.Compiler.MAlonzo.Compiler |
| hsCoerce | Agda.Compiler.MAlonzo.Compiler |
| HsDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| hsForall | Agda.Compiler.HaskellTypes |
| hsFun | Agda.Compiler.HaskellTypes |
| hsKFun | Agda.Compiler.HaskellTypes |
| hslit | Agda.Compiler.MAlonzo.Compiler |
| hsStar | Agda.Compiler.HaskellTypes |
| HsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsVar | Agda.Compiler.HaskellTypes |
| hsVarUQ | Agda.Compiler.MAlonzo.Misc |
| iBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ICArgList | Agda.Auto.Syntax |
| ICExp | Agda.Auto.Syntax |
| icnvh | Agda.Auto.Convert |
| Id | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| Ident | Agda.Syntax.Concrete |
| identifier | Agda.Syntax.Parser.LexActions |
| identity | Agda.Utils.TestHelpers |
| IdentP | Agda.Syntax.Concrete |
| idP | Agda.Utils.Permutation |
| IdPart | Agda.Syntax.Notation |
| idSub | Agda.TypeChecking.Substitute |
| iEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| If | Agda.Compiler.Epic.AuxAST |
| ifM | Agda.Utils.Monad |
| IgnoreAbstractMode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ignoreAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| ignoreBlocking | Agda.Syntax.Internal |
| ignoreForced | Agda.Syntax.Common |
| ignoreInterfaces | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| ignoreReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iHighlighting | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ihname | Agda.Compiler.MAlonzo.Misc |
| iImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iInsideScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IlltypedPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IM | Agda.Interaction.Monad |
| iModuleName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ImpInsert | Agda.TypeChecking.Implicit |
| impInsert | Agda.TypeChecking.Implicit |
| ImplicitInsertion | Agda.TypeChecking.Implicit |
| ImplicitP | Agda.Syntax.Abstract |
| Import | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| ImportDirective | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importDirRange | Agda.Syntax.Concrete |
| ImportedModule | Agda.Syntax.Concrete |
| ImportedName | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| importedName | Agda.Syntax.Concrete |
| importedNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ImportedNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ImportPragma | Agda.Syntax.Concrete |
| imports | Agda.Compiler.MAlonzo.Compiler |
| importsForPrim | Agda.Compiler.MAlonzo.Primitives |
| IMPOSSIBLE | Agda.Compiler.Epic.AuxAST |
| Impossible | |
| 1 (Type/Class) | Agda.Utils.Impossible |
| 2 (Data Constructor) | Agda.Utils.Impossible |
| ImpossiblePragma | Agda.Syntax.Concrete |
| impossibleTerm | Agda.Syntax.Internal |
| impossibleTest | Agda.ImpossibleTest |
| imp_dir | Agda.Syntax.Parser.Lexer |
| inAbstractMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inc | Agda.Utils.Warshall |
| InClause | Agda.TypeChecking.Positivity |
| IncompletePattern | Agda.Interaction.Highlighting.Precise |
| IncompletePatternMatching | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inConcreteMode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| inContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| InDefOf | Agda.TypeChecking.Positivity |
| indent | Agda.Utils.String |
| Independence | Agda.Interaction.GhciTop |
| independence | Agda.Interaction.GhciTop |
| Independent | Agda.Interaction.GhciTop |
| Index | |
| 1 (Data Constructor) | Agda.Utils.Suffix |
| 2 (Type/Class) | Agda.Termination.CallGraph |
| IndexFreeInParameter | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IndexVariablesNotDistinct | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| IndicesNotConstructorApplications | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Induction | Agda.Syntax.Common |
| Inductive | Agda.Syntax.Common |
| inductiveCheck | Agda.TypeChecking.Rules.Builtin |
| Inf | Agda.Syntax.Internal |
| InferDef | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferDef | Agda.TypeChecking.Rules.Term |
| InferExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inferExpr | Agda.TypeChecking.Rules.Term, Agda.TypeChecker, Agda.Interaction.GhciTop |
| inferHead | Agda.TypeChecking.Rules.Term |
| infertypevar | Agda.Auto.CaseSplit |
| InferVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| infimum | Agda.Termination.CallGraph |
| Infinite | Agda.Utils.Warshall |
| infinite | Agda.Utils.Warshall |
| Infix | Agda.Syntax.Concrete |
| InfixDef | Agda.Syntax.Common |
| infixlP | Agda.Syntax.Concrete.Operators.Parser |
| infixP | Agda.Syntax.Concrete.Operators.Parser |
| infixrP | Agda.Syntax.Concrete.Operators.Parser |
| Info | Agda.Syntax.Info |
| infodecl | Agda.Compiler.MAlonzo.Compiler |
| infoOnException | Agda.Interaction.GhciTop |
| initCompileState | Agda.Compiler.Epic.CompileState |
| initEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| initGraph | Agda.Utils.Warshall |
| initiate | Agda.Compiler.Epic.Erasure |
| initMapS | Agda.Auto.Convert |
| initMeta | Agda.Auto.NarrowingSearch |
| initState | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 3 (Function) | Agda.Interaction.GhciTop |
| Inline | Agda.Compiler.Epic.AuxAST |
| inMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| inNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| InScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| InScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inScopeTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| insert | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Termination.CallGraph |
| insertImplicit | Agda.TypeChecking.Implicit |
| insertImplicitPatterns | Agda.TypeChecking.Rules.LHS.Implicit |
| insertImplicitProblem | Agda.TypeChecking.Rules.LHS.Implicit |
| insertPatterns | Agda.TypeChecking.Rules.Def |
| insertTele | Agda.Compiler.Epic.Forcing |
| insertWithKeyM | Agda.Utils.Map |
| InsideOperandCtx | Agda.Syntax.Fixity |
| insideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| Instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiate | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| Instantiated | Agda.Interaction.BasicOps |
| instantiateDef | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| InstantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiateFull | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| instantiatePattern | Agda.TypeChecking.Rules.LHS |
| instantiateTel | Agda.TypeChecking.Rules.LHS.Instantiate |
| inState | Agda.Syntax.Parser.LexActions |
| InstS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InstV | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| int | Agda.Utils.Pretty |
| integer | Agda.Utils.Pretty |
| integerSemiring | Agda.Termination.Semiring |
| Interaction | |
| 1 (Type/Class) | Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Interaction.GhciTop |
| interaction | Agda.Interaction.CommandLine.CommandLine |
| InteractionId | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| interactionLoop | Agda.Interaction.CommandLine.CommandLine |
| InteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| interestingCall | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| Interface | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| InternalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| internalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| intersectWith | Agda.Termination.SparseMatrix |
| Interval | |
| 1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| intervalInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| intMap | Agda.Utils.Warshall |
| introTactic | Agda.Interaction.BasicOps |
| Inv | Agda.TypeChecking.Injectivity |
| InvalidPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Invariant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Inverse | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| inverseScopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inverseScopeLookupModule | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| inverseScopeLookupName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| invertP | Agda.Utils.Permutation |
| InvView | Agda.TypeChecking.Injectivity |
| io | Agda.TypeChecking.Primitive |
| IOException | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| iotapossmeta | Agda.Auto.Typecheck |
| iotastep | Agda.Auto.Typecheck |
| ioTCM | Agda.Interaction.GhciTop |
| ioTCM_ | Agda.Interaction.GhciTop |
| iPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Irr | Agda.Compiler.Epic.Erasure |
| irrBranch | Agda.Compiler.Epic.ConstructorIrrelevancy |
| Irrelevant | Agda.Syntax.Common |
| irrelevant | Agda.Syntax.Common |
| IrrelevantDatatype | Agda.TypeChecking.Coverage |
| irrExpr | Agda.Compiler.Epic.ConstructorIrrelevancy |
| IrrFilter | Agda.Compiler.Epic.CompileState |
| irrFilter | Agda.Compiler.Epic.ConstructorIrrelevancy |
| irrFilters | Agda.Compiler.Epic.CompileState |
| irrFun | Agda.Compiler.Epic.ConstructorIrrelevancy |
| IsAbstract | Agda.Syntax.Common |
| isAHole | Agda.Syntax.Notation |
| isBelow | Agda.Utils.Warshall |
| isBindingHole | Agda.Syntax.Notation |
| isBlockedTerm | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| isCoinductive | Agda.TypeChecking.Rules.Data |
| iScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isDatatype | |
| 1 (Function) | Agda.TypeChecking.Datatypes |
| 2 (Function) | Agda.TypeChecking.Coverage |
| IsEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isEmpty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.Termination.SparseMatrix |
| 3 (Function) | Agda.Termination.Matrix |
| IsEmptyType | Agda.Interaction.BasicOps |
| isEmptyType | Agda.TypeChecking.Empty |
| isEmptyTypeC | Agda.TypeChecking.Empty |
| isEtaExpandable | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| isEtaRecord | Agda.TypeChecking.Records |
| IsExpr | Agda.Syntax.Concrete.Operators.Parser |
| isGeneratedRecordConstructor | Agda.TypeChecking.Records |
| isHaskellKind | Agda.Compiler.HaskellTypes |
| isHiddenArg | Agda.Syntax.Common |
| isHole | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| iSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isImported | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isIn | Agda.Compiler.Epic.Forcing |
| isInCase | Agda.Compiler.Epic.Forcing |
| isIndependent | Agda.Interaction.GhciTop |
| IsInfix | Agda.Syntax.Common |
| isInfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isInModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isInstantiatedMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isInteractionMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isInTerm | Agda.Compiler.Epic.Forcing |
| isIrr | Agda.Compiler.Epic.Erasure |
| isJust | Agda.Utils.Maybe |
| isLambdaHole | Agda.Syntax.Notation |
| isLeft | Agda.Utils.Either |
| isLevelConstraint | Agda.TypeChecking.UniversePolymorphism |
| isLiterate | Agda.Interaction.Options |
| isNewerThan | Agda.Interaction.Imports |
| isNoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNonfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isNothing | Agda.Utils.Maybe |
| isntTypeConf | Agda.TypeChecking.Test.Generators |
| isOperator | |
| 1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isPostfix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isPrefix | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| isProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| isRec | Agda.Compiler.Epic.NatDetection |
| isRecord | Agda.TypeChecking.Records |
| isRecordConstructor | Agda.TypeChecking.Records |
| IsReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isRel | Agda.Compiler.Epic.Erasure |
| isRight | Agda.Utils.Either |
| isSingleton | Agda.Termination.SparseMatrix |
| isSingletonRecord | Agda.TypeChecking.Records |
| isSizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| isSolvedProblem | Agda.TypeChecking.Rules.LHS |
| IsSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isSortMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| isString | Agda.Utils.Generics |
| isSubModuleOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| isSuccess | Agda.Utils.QuickCheck |
| iStart | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| isType | Agda.TypeChecking.Rules.Term |
| IsTypeCall | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isTypeConf | Agda.TypeChecking.Test.Generators |
| IsType_ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| isType_ | Agda.TypeChecking.Rules.Term |
| isUnicodeId | Agda.Utils.Unicode |
| isVar | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| isVisited | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| isWellScoped | Agda.TypeChecking.Test.Generators |
| isZero | Agda.Utils.TestHelpers |
| Item | Agda.TypeChecking.Positivity |
| iterate' | Agda.Utils.Function |
| Judgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| judgementInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| judgToOutputForm | Agda.Interaction.BasicOps |
| Just | Agda.Utils.Maybe |
| JustSort | Agda.Interaction.BasicOps |
| JustType | Agda.Interaction.BasicOps |
| keepComments | Agda.Syntax.Parser.Comments |
| keepCommentsM | Agda.Syntax.Parser.Comments |
| Keyword | |
| 1 (Type/Class) | Agda.Syntax.Parser.Tokens |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| keyword | |
| 1 (Function) | Agda.Syntax.Parser.LexActions |
| 2 (Function) | Agda.Interaction.Highlighting.Vim |
| killAbs | Agda.TypeChecking.Test.Generators |
| killArgs | Agda.TypeChecking.MetaVars.Occurs |
| killedType | Agda.TypeChecking.MetaVars.Occurs |
| KillRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange1 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange2 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange3 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange4 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange5 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange6 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| killRange7 | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| KillVar | Agda.TypeChecking.Test.Generators |
| killVar | Agda.TypeChecking.Test.Generators |
| KindOfName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| KwAbstract | Agda.Syntax.Parser.Tokens |
| KwBUILTIN | Agda.Syntax.Parser.Tokens |
| KwCoData | Agda.Syntax.Parser.Tokens |
| KwCOMPILED | Agda.Syntax.Parser.Tokens |
| KwCOMPILED_DATA | Agda.Syntax.Parser.Tokens |
| KwCOMPILED_EPIC | Agda.Syntax.Parser.Tokens |
| KwCOMPILED_TYPE | Agda.Syntax.Parser.Tokens |
| KwConstructor | Agda.Syntax.Parser.Tokens |
| KwData | Agda.Syntax.Parser.Tokens |
| KwETA | Agda.Syntax.Parser.Tokens |
| KwField | Agda.Syntax.Parser.Tokens |
| KwForall | Agda.Syntax.Parser.Tokens |
| KwHiding | Agda.Syntax.Parser.Tokens |
| KwIMPORT | Agda.Syntax.Parser.Tokens |
| KwImport | Agda.Syntax.Parser.Tokens |
| KwIMPOSSIBLE | Agda.Syntax.Parser.Tokens |
| KwIn | Agda.Syntax.Parser.Tokens |
| KwInfix | Agda.Syntax.Parser.Tokens |
| KwInfixL | Agda.Syntax.Parser.Tokens |
| KwInfixR | Agda.Syntax.Parser.Tokens |
| KwLet | Agda.Syntax.Parser.Tokens |
| KwLINE | Agda.Syntax.Parser.Tokens |
| KwModule | Agda.Syntax.Parser.Tokens |
| KwMutual | Agda.Syntax.Parser.Tokens |
| KwOpen | Agda.Syntax.Parser.Tokens |
| KwOPTIONS | Agda.Syntax.Parser.Tokens |
| KwPostulate | Agda.Syntax.Parser.Tokens |
| KwPrimitive | Agda.Syntax.Parser.Tokens |
| KwPrivate | Agda.Syntax.Parser.Tokens |
| KwProp | Agda.Syntax.Parser.Tokens |
| KwPublic | Agda.Syntax.Parser.Tokens |
| KwQuote | Agda.Syntax.Parser.Tokens |
| KwQuoteGoal | Agda.Syntax.Parser.Tokens |
| KwRecord | Agda.Syntax.Parser.Tokens |
| KwRenaming | Agda.Syntax.Parser.Tokens |
| KwRewrite | Agda.Syntax.Parser.Tokens |
| KwSet | Agda.Syntax.Parser.Tokens |
| KwSyntax | Agda.Syntax.Parser.Tokens |
| KwTo | Agda.Syntax.Parser.Tokens |
| KwUsing | Agda.Syntax.Parser.Tokens |
| KwWhere | Agda.Syntax.Parser.Tokens |
| KwWith | Agda.Syntax.Parser.Tokens |
| L | |
| 1 (Data Constructor) | Agda.Utils.Map |
| 2 (Data Constructor) | Agda.Interaction.GhciTop |
| label | Agda.Utils.QuickCheck |
| labels | Agda.Utils.QuickCheck |
| Lam | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| lambda | Agda.Syntax.Concrete.Pretty |
| LambdaHole | Agda.Syntax.Notation |
| lambdaLift | Agda.Compiler.Epic.LambdaLift |
| lambdaLiftExpr | Agda.Compiler.Epic.LambdaLift |
| lambdaLiftFun | Agda.Compiler.Epic.LambdaLift |
| LamBinding | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Abstract |
| lamBrackets | Agda.Syntax.Fixity |
| lamFreq | Agda.TypeChecking.Test.Generators |
| LamV | Agda.Syntax.Concrete.Operators.Parser |
| Layout | Agda.Syntax.Parser.Monad |
| layout | Agda.Syntax.Parser.Lexer |
| LayoutContext | Agda.Syntax.Parser.Monad |
| layoutKeywords | Agda.Syntax.Parser.Tokens |
| Lazy | Agda.Compiler.Epic.AuxAST |
| lbrace | Agda.Utils.Pretty |
| lbrack | Agda.Utils.Pretty |
| LChar | Agda.Compiler.Epic.AuxAST |
| le | Agda.Termination.CallGraph |
| LeftAssoc | Agda.Syntax.Fixity |
| LeftDisjunct | Agda.Auto.NarrowingSearch |
| leftDistributive | Agda.Utils.TestHelpers |
| LeftHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LeftMode | Agda.Utils.Pretty |
| LeftOfArrow | Agda.TypeChecking.Positivity |
| LeftOperandCtx | Agda.Syntax.Fixity |
| LegendMatrix | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.Utils.Warshall |
| Leq | Agda.TypeChecking.SizedTypes |
| leqLevel | Agda.TypeChecking.Conversion |
| leqSort | Agda.TypeChecking.Conversion |
| leqType | Agda.TypeChecking.Conversion |
| Let | |
| 1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| LetApply | Agda.Syntax.Abstract |
| LetBind | Agda.Syntax.Abstract |
| LetBinding | Agda.Syntax.Abstract |
| LetBindings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| LetDef | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LetDefs | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LetInfo | Agda.Syntax.Info |
| LetOpen | Agda.Syntax.Abstract |
| LetRange | Agda.Syntax.Info |
| LevelAtom | Agda.TypeChecking.Level |
| LevelCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| LevelKit | |
| 1 (Type/Class) | Agda.TypeChecking.Level |
| 2 (Data Constructor) | Agda.TypeChecking.Level |
| levelMax | Agda.TypeChecking.Level |
| Levels | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| levelSuc | Agda.TypeChecking.Level |
| levelSucFunction | Agda.TypeChecking.Level |
| levelType | Agda.TypeChecking.Level |
| LevelView | Agda.TypeChecking.Level |
| levelView | Agda.TypeChecking.Level |
| levelZero | Agda.TypeChecking.Level |
| LexAction | Agda.Syntax.Parser.Alex |
| lexer | Agda.Syntax.Parser.Lexer |
| lexError | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser.LexActions |
| lexInput | Agda.Syntax.Parser.Alex |
| LexOrder | Agda.Termination.Lexicographic |
| lexOrder | Agda.Termination.Lexicographic |
| lexPos | Agda.Syntax.Parser.Alex |
| LexPredicate | Agda.Syntax.Parser.Alex |
| lexPrevChar | Agda.Syntax.Parser.Alex |
| LexState | Agda.Syntax.Parser.Monad |
| lexToken | Agda.Syntax.Parser.LexActions |
| LFloat | Agda.Compiler.Epic.AuxAST |
| LHS | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| LHSInfo | Agda.Syntax.Info |
| LHSRange | Agda.Syntax.Info |
| lift | Agda.Auto.CaseSplit |
| lift2 | Agda.Compiler.Epic.Forcing |
| liftEither | Agda.Utils.Monad |
| liftP | Agda.Syntax.Parser.LookAhead |
| liftTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| lineLength | Agda.Utils.Pretty |
| LInt | Agda.Compiler.Epic.AuxAST |
| Lisp | Agda.Interaction.GhciTop |
| list | Agda.TypeChecking.Primitive |
| listenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| listOf | Agda.Utils.QuickCheck |
| listOf1 | Agda.Utils.QuickCheck |
| listOfElements | Agda.Utils.TestHelpers |
| listToMaybe | Agda.Utils.Maybe |
| Lit | |
| 1 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 2 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| litBranches | Agda.TypeChecking.CompiledClause |
| litCase | Agda.TypeChecking.CompiledClause |
| LitChar | Agda.Syntax.Literal |
| litChar | Agda.Syntax.Parser.StringLiterals |
| Literal | Agda.Syntax.Literal |
| literal | |
| 1 (Function) | Agda.Syntax.Parser.LexActions |
| 2 (Function) | Agda.Compiler.MAlonzo.Compiler |
| literate | Agda.Syntax.Parser.Lexer |
| LitFloat | Agda.Syntax.Literal |
| LitFocus | Agda.TypeChecking.Rules.LHS.Problem |
| litFreq | Agda.TypeChecking.Test.Generators |
| LitInt | Agda.Syntax.Literal |
| LitLevel | Agda.Syntax.Literal |
| LitMP | Agda.TypeChecking.Coverage.Match |
| LitP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| LitQName | Agda.Syntax.Literal |
| LitString | Agda.Syntax.Literal |
| litString | Agda.Syntax.Parser.StringLiterals |
| litType | Agda.TypeChecking.Rules.Term |
| LL | Agda.Compiler.Epic.LambdaLift |
| loadFile | Agda.Interaction.CommandLine.CommandLine |
| localNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| localScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| localTerminationEnv | Agda.Auto.CaseSplit |
| localTerminationSidecond | Agda.Auto.CaseSplit |
| localToAbstract | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| LocalV | Agda.Syntax.Concrete.Operators.Parser |
| LocalVars | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| LocalVsImportedModuleClash | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| look | Agda.Utils.ReadP |
| LookAhead | Agda.Syntax.Parser.LookAhead |
| lookup | Agda.Utils.Graph |
| lookupConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| lookupEdge | Agda.Utils.Warshall |
| lookupInteractionId | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| lookupMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| lookupMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| lookupPath | Agda.Utils.Trie |
| lookupPrimitiveFunction | Agda.TypeChecking.Primitive |
| lookupSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| LowerMeta | Agda.Interaction.GhciTop |
| lowerMeta | Agda.Interaction.GhciTop |
| lowMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| lparen | Agda.Utils.Pretty |
| LString | Agda.Compiler.Epic.AuxAST |
| lt | Agda.Termination.CallGraph |
| Lub | Agda.Syntax.Internal |
| Lvl | |
| 1 (Type/Class) | Agda.TypeChecking.Primitive |
| 2 (Data Constructor) | Agda.TypeChecking.Primitive |
| main | Agda.Main |
| mainName | Agda.Compiler.Epic.CompileState |
| makeAbstract | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| makeAbstractClause | Agda.Interaction.MakeCase |
| makeAbsurdClause | Agda.Interaction.MakeCase |
| makeCase | Agda.Interaction.MakeCase |
| makeClosed | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
| makeConfiguration | Agda.TypeChecking.Test.Generators |
| makeEnv | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| makeIrrelevant | Agda.Syntax.Common |
| makeOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad |
| makeRelevant | Agda.Syntax.Common |
| makeSilent | Agda.Interaction.GhciTop |
| makeSubstitution | Agda.TypeChecking.Rules.LHS.Unify |
| MAlonzo | Agda.Interaction.GhciTop |
| many | Agda.Utils.ReadP |
| many1 | Agda.Utils.ReadP |
| manyTill | Agda.Utils.ReadP |
| mapCon | Agda.Compiler.Epic.Primitive |
| mapFlag | Agda.Interaction.Options |
| mapMaybe | Agda.Utils.Maybe |
| mapMaybeM | Agda.Utils.Monad |
| mapNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapNameSpaceM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapNodes | Agda.Utils.Warshall |
| MapS | Agda.Auto.Convert |
| mapScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapScopeM | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapScopeM_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapScope_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mapSize | Agda.Utils.QuickCheck |
| mapTCMT | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MArgList | Agda.Auto.Syntax |
| Mat | Agda.Termination.CallGraph |
| mat | Agda.Termination.CallGraph |
| Match | |
| 1 (Type/Class) | Agda.TypeChecking.Coverage.Match |
| 2 (Type/Class) | Agda.TypeChecking.Patterns.Match |
| 3 (Type/Class) | Agda.TypeChecking.DisplayForm |
| match | |
| 1 (Function) | Agda.TypeChecking.Coverage.Match |
| 2 (Function) | Agda.Syntax.Parser.LookAhead |
| 3 (Function) | Agda.Interaction.Highlighting.Vim |
| 4 (Function) | Agda.TypeChecking.DisplayForm |
| 5 (Function) | Agda.TypeChecking.CompiledClause.Match |
| match' | |
| 1 (Function) | Agda.Syntax.Parser.LookAhead |
| 2 (Function) | Agda.TypeChecking.CompiledClause.Match |
| matchClause | Agda.TypeChecking.Coverage.Match |
| matchCommand | Agda.Interaction.CommandLine.CommandLine |
| matchCompiled | Agda.TypeChecking.CompiledClause.Match |
| matchDisplayForm | Agda.TypeChecking.DisplayForm |
| matches | Agda.Interaction.Highlighting.Vim |
| MatchLit | Agda.TypeChecking.Coverage.Match |
| matchLits | Agda.TypeChecking.Coverage.Match |
| matchPat | Agda.TypeChecking.Coverage.Match |
| matchPats | Agda.TypeChecking.Coverage.Match |
| matchPattern | Agda.TypeChecking.Patterns.Match |
| matchPatterns | Agda.TypeChecking.Patterns.Match |
| matchType | Agda.Auto.Convert |
| Matrix | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Type/Class) | Agda.Termination.Matrix |
| 3 (Type/Class) | Agda.Utils.Warshall |
| matrix | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| 3 (Function) | Agda.Utils.Warshall |
| matrixInvariant | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| matrixUsingRowGen | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| Max | Agda.TypeChecking.Level |
| maxDiscard | Agda.Utils.QuickCheck |
| maxName | Agda.TypeChecking.Level |
| maxSize | Agda.Utils.QuickCheck |
| maxSuccess | Agda.Utils.QuickCheck |
| Maybe | Agda.Utils.Maybe |
| maybe | Agda.Utils.Maybe |
| maybeCoGen | Agda.Utils.TestHelpers |
| maybeGen | Agda.Utils.TestHelpers |
| maybeor | Agda.Auto.Typecheck |
| maybeOriginalClause | Agda.Syntax.Internal |
| maybePrefixMatch | Agda.Utils.List |
| maybePrimCon | Agda.TypeChecking.Level |
| maybePrimDef | Agda.TypeChecking.Level |
| MaybeRed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MaybeReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MaybeReducedArgs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| maybeToList | Agda.Utils.Maybe |
| mazBoolToHBool | Agda.Compiler.MAlonzo.Primitives |
| mazCharToInteger | Agda.Compiler.MAlonzo.Primitives |
| mazCoerce | Agda.Compiler.MAlonzo.Misc |
| mazerror | Agda.Compiler.MAlonzo.Misc |
| mazHBoolToBool | Agda.Compiler.MAlonzo.Primitives |
| mazHListToList | Agda.Compiler.MAlonzo.Primitives |
| mazIntegerToNat | Agda.Compiler.MAlonzo.Primitives |
| mazIntToNat | Agda.Compiler.MAlonzo.Primitives |
| mazListToHList | Agda.Compiler.MAlonzo.Primitives |
| mazListToString | Agda.Compiler.MAlonzo.Primitives |
| mazMod | Agda.Compiler.MAlonzo.Misc |
| mazMod' | Agda.Compiler.MAlonzo.Misc |
| mazName | Agda.Compiler.MAlonzo.Misc |
| mazNatToInt | Agda.Compiler.MAlonzo.Primitives |
| mazNatToInteger | Agda.Compiler.MAlonzo.Primitives |
| mazRTE | Agda.Compiler.MAlonzo.Misc |
| mazstr | Agda.Compiler.MAlonzo.Misc |
| mazStringToList | Agda.Compiler.MAlonzo.Primitives |
| MB | Agda.Auto.NarrowingSearch |
| mbcase | Agda.Auto.NarrowingSearch |
| mbfailed | Agda.Auto.NarrowingSearch |
| mbind | Agda.Auto.NarrowingSearch |
| mbpcase | Agda.Auto.NarrowingSearch |
| mbret | Agda.Auto.NarrowingSearch |
| mcompoint | Agda.Auto.NarrowingSearch |
| mergeInterface | Agda.Interaction.Imports |
| mergeNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mergeScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| mergeScopes | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Meta | Agda.Auto.NarrowingSearch |
| MetaArg | Agda.TypeChecking.Positivity |
| MetaCannotDependOn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaEnv | Agda.Auto.NarrowingSearch |
| MetaId | |
| 1 (Type/Class) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Internal |
| MetaInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| 3 (Type/Class) | Agda.Interaction.Highlighting.Precise |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 5 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaInstance | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| MetaInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaKind | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| MetaLevel | Agda.TypeChecking.Level |
| metaliseokh | Agda.Auto.Syntax |
| metaNumber | Agda.Syntax.Info |
| MetaOccursInItself | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaParseExpr | Agda.Interaction.CommandLine.CommandLine |
| MetaPriority | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaRange | Agda.Syntax.Info |
| MetaS | Agda.Syntax.Internal |
| metaScope | Agda.Syntax.Info |
| MetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MetaV | Agda.Syntax.Internal |
| MetaVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Metavar | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| MetaVariable | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| metaVariable | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| meta_not_constructor | Agda.Auto.Typecheck |
| MExp | Agda.Auto.Syntax |
| mextrarefs | Agda.Auto.NarrowingSearch |
| mhead | Agda.Utils.List |
| MId | Agda.Auto.Syntax |
| miInterface | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| minfoAsName | Agda.Syntax.Info |
| minfoAsTo | Agda.Syntax.Info |
| minfoDirective | Agda.Syntax.Info |
| minfoOpenShort | Agda.Syntax.Info |
| minfoRange | Agda.Syntax.Info |
| MissingDefinition | Agda.Syntax.Concrete.Definitions |
| MissingTypeSignature | Agda.Syntax.Concrete.Definitions |
| MissingWithClauses | Agda.Syntax.Concrete.Definitions |
| miTimeStamp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| miWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MIx | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| 3 (Type/Class) | Agda.Termination.Matrix |
| 4 (Data Constructor) | Agda.Termination.Matrix |
| mIxInvariant | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| mkAbsolute | Agda.Utils.FileName, Agda.Interaction.GhciTop |
| mkBoundName_ | Agda.Syntax.Concrete |
| mkCon | Agda.Compiler.Epic.Forcing |
| mkContextEntry | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| mkDefInfo | Agda.Syntax.Info |
| mkMatrix | Agda.Utils.Warshall |
| mkName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mkName_ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mkNotation | Agda.Syntax.Notation |
| mkPrimFun1 | Agda.TypeChecking.Primitive |
| mkPrimFun2 | Agda.TypeChecking.Primitive |
| mkPrimFun4 | Agda.TypeChecking.Primitive |
| MkStr | Agda.Utils.QuickCheck |
| mkType | Agda.Syntax.Internal |
| mlevel | Agda.TypeChecking.UniversePolymorphism |
| MM | Agda.Auto.NarrowingSearch |
| mm | Agda.Auto.CaseSplit |
| mmbpcase | Agda.Auto.NarrowingSearch |
| mmcase | Agda.Auto.NarrowingSearch |
| mmmcase | Agda.Auto.NarrowingSearch |
| mmpcase | Agda.Auto.NarrowingSearch |
| MName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| mobs | Agda.Auto.NarrowingSearch |
| Mode | Agda.Utils.Pretty |
| mode | Agda.Utils.Pretty |
| modifyAbstractClause | Agda.Auto.Convert |
| modifyAbstractExpr | Agda.Auto.Convert |
| modifyCurrentNameSpace | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyCurrentScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyCurrentScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| modifyM | Agda.Compiler.Epic.Forcing |
| modifyNamedScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyNamedScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| modifyScopeInfo | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifyScopes | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| modifySignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| modSub | Agda.TypeChecking.Rules.LHS.Unify |
| Module | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| ModuleArityMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| moduleContents | Agda.Interaction.BasicOps |
| ModuleDefinedInOtherFile | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ModuleDoesntExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ModuleInfo | |
| 1 (Type/Class) | Agda.Syntax.Info |
| 2 (Data Constructor) | Agda.Syntax.Info |
| 3 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ModuleMacro | Agda.Syntax.Concrete |
| ModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| moduleName | Agda.Interaction.FindFile |
| moduleName' | Agda.Interaction.FindFile |
| ModuleNameDoesntMatchFileName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| moduleNameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleNameToFileName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| moduleParser | |
| 1 (Function) | Agda.Syntax.Parser.Parser |
| 2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ModulesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ModuleTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ModuleToSource | Agda.Interaction.FindFile |
| MonadException | Agda.TypeChecking.Monad.Exception |
| MonadTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| movePos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| movePosByString | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| mparen | Agda.Syntax.Concrete.Operators |
| mparens | Agda.Utils.Pretty |
| MPat | Agda.TypeChecking.Coverage.Match |
| mpret | Agda.Auto.NarrowingSearch |
| mprincipalpresent | Agda.Auto.NarrowingSearch |
| mul | |
| 1 (Function) | Agda.Termination.Semiring |
| 2 (Function) | Agda.Termination.SparseMatrix |
| 3 (Function) | Agda.Termination.Matrix |
| MultipleFixityDecls | Agda.Syntax.Concrete.Definitions |
| multiply | Agda.Termination.Semiring |
| munch | Agda.Utils.ReadP |
| munch1 | Agda.Utils.ReadP |
| MutId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Mutual | Agda.Syntax.Concrete |
| MutualId | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvInstantiation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvJudgement | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvListeners | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvPermutation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| mvPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| MyMB | Agda.Auto.Syntax |
| MyPB | Agda.Auto.Syntax |
| Name | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| 4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| 5 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| nameBindingSite | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| nameConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| Named | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| named | Agda.Syntax.Common |
| NamedArg | Agda.Syntax.Common |
| NamedClause | |
| 1 (Type/Class) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| namedThing | Agda.Syntax.Common |
| nameFixity | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| nameFreq | Agda.TypeChecking.Test.Generators |
| NameFreqs | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| nameFreqs | Agda.TypeChecking.Test.Generators |
| NameId | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Common |
| nameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| NameKind | Agda.Interaction.Highlighting.Precise |
| nameModifiers | Agda.Interaction.GhciTop |
| nameOf | Agda.Syntax.Common |
| nameOfBV | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| nameOfFlat | Agda.TypeChecking.Rules.Builtin.Coinduction |
| nameOfInf | Agda.TypeChecking.Rules.Builtin.Coinduction |
| nameOfSharp | Agda.TypeChecking.Rules.Builtin.Coinduction |
| NamePart | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| nameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NamesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| namesInScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| NameSpace | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| NameSpaceId | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| nameSupply | Agda.Compiler.Epic.CompileState |
| NameTag | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Nat | |
| 1 (Type/Class) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Syntax.Common |
| 3 (Type/Class) | Agda.TypeChecking.Primitive |
| 4 (Data Constructor) | Agda.TypeChecking.Primitive |
| natPrimTF | Agda.Compiler.Epic.Primitive |
| natural | Agda.Utils.TestHelpers |
| neg | Agda.TypeChecking.Polarity |
| Negative | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| negtype | Agda.Auto.Convert |
| neighbours | Agda.Utils.Graph |
| nest | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| nestedComment | Agda.Syntax.Parser.Comments |
| NeutralLevel | Agda.TypeChecking.Level |
| newArgsMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newArgsMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newCTree | Agda.Auto.NarrowingSearch |
| newEdge | Agda.Utils.Warshall |
| NewFlex | Agda.Utils.Warshall |
| newLayoutContext | Agda.Syntax.Parser.Layout |
| newMeta | |
| 1 (Function) | Agda.Auto.NarrowingSearch |
| 2 (Function) | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| newMeta' | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| NewModuleName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| NewModuleQName | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| NewName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| newName | Agda.Compiler.Epic.CompileState |
| NewNotation | Agda.Syntax.Fixity |
| newOKHandle | Agda.Auto.NarrowingSearch |
| newPlaceholder | Agda.Auto.NarrowingSearch |
| newQuestionMark | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newRecordMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newRecordMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newSortMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newSortMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newSubConstraints | Agda.Auto.NarrowingSearch |
| newTelMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newTypeMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newTypeMeta_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newValueMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newValueMeta' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newValueMetaCtx | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| newValueMetaCtx' | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| nextChar | Agda.Syntax.Parser.LookAhead |
| nextFresh | Agda.Utils.Fresh |
| nextName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| nextNode | Agda.Utils.Warshall |
| nextPolarity | Agda.TypeChecking.Conversion |
| nextSplit | Agda.TypeChecking.CompiledClause |
| nextSuffix | Agda.Utils.Suffix |
| Nice | Agda.Syntax.Concrete.Definitions |
| NiceConstructor | Agda.Syntax.Concrete.Definitions |
| NiceDeclaration | Agda.Syntax.Concrete.Definitions |
| niceDeclarations | Agda.Syntax.Concrete.Definitions |
| NiceDef | Agda.Syntax.Concrete.Definitions |
| NiceDefinition | Agda.Syntax.Concrete.Definitions |
| NiceField | Agda.Syntax.Concrete.Definitions |
| NiceImport | Agda.Syntax.Concrete.Definitions |
| NiceModule | Agda.Syntax.Concrete.Definitions |
| NiceModuleMacro | Agda.Syntax.Concrete.Definitions |
| NiceOpen | Agda.Syntax.Concrete.Definitions |
| NicePragma | Agda.Syntax.Concrete.Definitions |
| NiceTypeSignature | Agda.Syntax.Concrete.Definitions |
| No | |
| 1 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| NoApp | Agda.TypeChecking.EtaContract |
| NoBind | Agda.Syntax.Internal |
| NoBindingForBuiltin | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noblks | Agda.Auto.Typecheck |
| NoBody | Agda.Syntax.Internal |
| noConstraints | Agda.TypeChecking.Constraints |
| Node | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.Positivity |
| NodeId | Agda.Utils.Warshall |
| nodeMap | Agda.Utils.Warshall |
| nodes | Agda.Utils.Graph |
| NoExpectedFailure | Agda.Utils.QuickCheck |
| noFixity | Agda.Syntax.Fixity |
| NoFunV | Agda.Syntax.Internal |
| NoId | Agda.Auto.Syntax |
| NoInsertNeeded | Agda.TypeChecking.Implicit |
| NoInv | Agda.TypeChecking.Injectivity |
| noiotastep | Agda.Auto.Typecheck |
| noiotastep_term | Agda.Auto.Typecheck |
| NoLayout | Agda.Syntax.Parser.Monad |
| noLiterals | Agda.TypeChecking.Test.Generators |
| noMatchLit | Agda.TypeChecking.Coverage.Match |
| noModuleName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| noMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| NoName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| noName | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| noName_ | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| NonApplication | Agda.Syntax.Abstract.Views |
| NonAssoc | Agda.Syntax.Fixity |
| NonEmpty | Agda.Utils.QuickCheck |
| NonEmptyList | Agda.Utils.QuickCheck |
| nonfixP | Agda.Syntax.Concrete.Operators.Parser |
| NonNegative | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| noNotation | Agda.Syntax.Notation |
| NonPositively | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NonZero | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| NoParseForApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoParseForLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noPatternMatchingOnCodata | Agda.TypeChecking.Rules.LHS |
| Nope | Agda.Syntax.Info |
| NoPrio | Agda.Auto.NarrowingSearch |
| noProp | Agda.TypeChecking.Test.Generators |
| noRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| NoRecordConstructor | Agda.TypeChecking.Coverage |
| NoReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoRHSRequiresAbsurdPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| norm | Agda.Auto.Convert |
| normal | Agda.Syntax.Parser.Lexer |
| NormalHole | Agda.Syntax.Notation |
| Normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| normalise | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| Normalised | Agda.Interaction.BasicOps |
| normalMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| noShadowingOfConstructors | Agda.TypeChecking.Rules.LHS |
| noShrink | Agda.TypeChecking.Test.Generators |
| NoSuchBuiltinName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuchModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuchName | Agda.TypeChecking.Implicit |
| NoSuchPrimitiveFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoSuffix | Agda.Utils.Suffix |
| not' | Agda.Syntax.Parser.Alex |
| NotADatatype | Agda.TypeChecking.Coverage |
| notAHaskellKind | Agda.Compiler.HaskellTypes |
| notAHaskellType | Agda.Compiler.HaskellTypes |
| NotAllowedInMutual | Agda.Syntax.Concrete.Definitions |
| NotAModuleExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotAnExpression | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotAProperTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Notation | Agda.Syntax.Notation |
| NotAValidLetBinding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotB | Agda.Auto.NarrowingSearch |
| NotBlocked | Agda.Syntax.Internal |
| notBlocked | Agda.Syntax.Internal |
| NotDelayed | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| note | Agda.Interaction.Highlighting.Precise |
| notequal | Agda.Auto.CaseSplit |
| NotFound | Agda.Interaction.FindFile |
| NotHidden | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Common |
| notHiddenFreq | Agda.TypeChecking.Test.Generators |
| Nothing | Agda.Utils.Maybe |
| NothingAppliedToHiddenArg | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NothingToSplit | Agda.TypeChecking.Rules.LHS.Problem |
| nothingToSplitError | Agda.TypeChecking.Rules.LHS.Instantiate |
| NotImplemented | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInductive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInjective | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotInScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notInScope | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| NotLeqSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotM | Agda.Auto.NarrowingSearch |
| NotPB | Agda.Auto.NarrowingSearch |
| NotReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notReduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| notSoNiceDeclarations | Agda.Syntax.Concrete.Definitions |
| NotStrictlyPositive | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NotSupported | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| NoType | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| NoUnify | Agda.TypeChecking.Rules.LHS.Unify |
| NoWhere | Agda.Syntax.Concrete |
| NoWithFunction | Agda.TypeChecking.Rules.Def |
| nPi | Agda.TypeChecking.Primitive |
| nrRel | Agda.Compiler.Epic.NatDetection |
| nsModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| nsNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Number | Agda.Interaction.Highlighting.Precise |
| numShrinks | Agda.Utils.QuickCheck |
| numTests | Agda.Utils.QuickCheck |
| O | Agda.Auto.Convert |
| Occ | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| OccPos | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| occPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Occurrence | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Occurrences | Agda.TypeChecking.Positivity |
| occurrences | Agda.TypeChecking.Positivity |
| Occurs | Agda.TypeChecking.MetaVars.Occurs |
| occurs | Agda.TypeChecking.MetaVars.Occurs |
| occursAs | Agda.TypeChecking.Positivity |
| occursCheck | |
| 1 (Function) | Agda.TypeChecking.MetaVars.Occurs |
| 2 (Function) | Agda.TypeChecking.Rules.LHS.Unify |
| OccursCtx | Agda.TypeChecking.MetaVars.Occurs |
| OccursWhere | Agda.TypeChecking.Positivity |
| octDigit | Agda.Utils.Char |
| ofExpr | Agda.Interaction.BasicOps |
| offsideRule | Agda.Syntax.Parser.Layout |
| ofName | Agda.Interaction.BasicOps |
| OfType | Agda.Interaction.BasicOps |
| OfType' | Agda.Interaction.BasicOps |
| OHCon | Agda.Syntax.Internal.Pattern |
| OHPats | Agda.Syntax.Internal.Pattern |
| OK | Agda.Auto.NarrowingSearch |
| OKHandle | Agda.Auto.NarrowingSearch |
| OKMeta | Agda.Auto.NarrowingSearch |
| OKVal | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| OldModuleName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| OldName | |
| 1 (Type/Class) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| OldQName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| oldToNewNotation | Agda.Syntax.Fixity |
| on | Agda.Interaction.Highlighting.Vim |
| OneHolePattern | Agda.Syntax.Internal.Pattern |
| OneHolePatterns | Agda.Syntax.Internal.Pattern |
| OneLineMode | Agda.Utils.Pretty |
| oneof | Agda.Utils.QuickCheck |
| onSub | Agda.TypeChecking.Rules.LHS.Unify |
| Op | Agda.TypeChecking.Primitive |
| OpApp | Agda.Syntax.Concrete |
| OpAppP | Agda.Syntax.Concrete |
| OpAppV | Agda.Syntax.Concrete.Operators.Parser |
| opBrackets | Agda.Syntax.Fixity |
| Open | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 4 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| openBrace | Agda.Syntax.Parser.Layout |
| openModule_ | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| OpenShortHand | Agda.Syntax.Concrete |
| OpenThing | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| oplus | Agda.Utils.SemiRing |
| opP | Agda.Syntax.Concrete.Operators.Parser |
| optAllowUnsolved | Agda.Interaction.Options |
| optCompile | Agda.Interaction.Options |
| optCompileDir | Agda.Interaction.Options |
| optCompletenessCheck | Agda.Interaction.Options |
| optCSSFile | Agda.Interaction.Options |
| optDisablePositivity | Agda.Interaction.Options |
| optEpicCompile | Agda.Interaction.Options |
| optEpicFlags | Agda.Interaction.Options |
| optForcing | Agda.Interaction.Options |
| optGenerateHTML | Agda.Interaction.Options |
| optGenerateVimFile | Agda.Interaction.Options |
| optGhcFlags | Agda.Interaction.Options |
| optGuardingTypeConstructors | Agda.Interaction.Options |
| optHTMLDir | Agda.Interaction.Options |
| optIgnoreInterfaces | Agda.Interaction.Options |
| optIncludeDirs | Agda.Interaction.Options |
| optInjectiveTypeConstructors | Agda.Interaction.Options |
| optInputFile | Agda.Interaction.Options |
| optInteractive | Agda.Interaction.Options |
| option | Agda.Utils.ReadP |
| optional | Agda.Utils.ReadP |
| optionError | Agda.Main |
| Options | Agda.Interaction.Options |
| OptionsPragma | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Type/Class) | Agda.Interaction.Options |
| optIrrelevantProjections | Agda.Interaction.Options |
| optPragmaOptions | Agda.Interaction.Options |
| optProgramName | Agda.Interaction.Options |
| optProofIrrelevance | Agda.Interaction.Options |
| optRunTests | Agda.Interaction.Options |
| optShowHelp | Agda.Interaction.Options |
| optShowImplicit | Agda.Interaction.Options |
| optShowVersion | Agda.Interaction.Options |
| optSizedTypes | Agda.Interaction.Options |
| optTerminationCheck | Agda.Interaction.Options |
| optTerminationDepth | Agda.Interaction.Options |
| optUniverseCheck | Agda.Interaction.Options |
| optUniversePolymorphism | Agda.Interaction.Options |
| optUnreachableCheck | Agda.Interaction.Options |
| optVerbose | Agda.Interaction.Options |
| optWithoutK | Agda.Interaction.Options |
| Or | Agda.Auto.NarrowingSearch |
| Order | Agda.Termination.CallGraph |
| Ordered | Agda.Utils.QuickCheck |
| OrderedList | Agda.Utils.QuickCheck |
| orderedList | Agda.Utils.QuickCheck |
| orderFields | Agda.TypeChecking.Records |
| orderMat | Agda.Termination.CallGraph |
| originalClause | Agda.Syntax.Internal |
| OtherAspect | Agda.Interaction.Highlighting.Precise |
| otherAspects | Agda.Interaction.Highlighting.Precise |
| OtherSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| OtherV | Agda.Syntax.Concrete.Operators.Parser |
| otimes | Agda.Utils.SemiRing |
| Out | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| outFile | Agda.Compiler.MAlonzo.Compiler |
| outFile' | Agda.Compiler.MAlonzo.Compiler |
| outFile_ | Agda.Compiler.MAlonzo.Compiler |
| output | Agda.Utils.QuickCheck |
| OutputForm | Agda.Interaction.BasicOps |
| OutputForm' | Agda.Interaction.BasicOps |
| outputFormId | Agda.Interaction.BasicOps |
| outsideScope | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| overlapping | Agda.Interaction.Highlighting.Range |
| OverlappingProjects | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PageMode | Agda.Utils.Pretty |
| Pair | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| pairwiseFilter | Agda.Compiler.Epic.AuxAST |
| Paren | Agda.Syntax.Concrete |
| paren | Agda.Syntax.Concrete.Operators |
| ParenP | Agda.Syntax.Concrete |
| parens | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| ParenV | Agda.Syntax.Concrete.Operators.Parser |
| parse | |
| 1 (Function) | Agda.Utils.ReadP |
| 2 (Function) | Agda.Syntax.Parser.Monad |
| 3 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parseAndDoAtToplevel | Agda.Interaction.GhciTop |
| parseApplication | Agda.Syntax.Concrete.Operators |
| ParseError | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Parser.Monad, Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parseError | Agda.Syntax.Parser.Monad |
| parseErrorAt | Agda.Syntax.Parser.Monad |
| parseExpr | |
| 1 (Function) | Agda.Interaction.BasicOps |
| 2 (Function) | Agda.Interaction.CommandLine.CommandLine |
| parseExprIn | Agda.Interaction.BasicOps |
| ParseFailed | Agda.Syntax.Parser.Monad |
| parseFile | Agda.Syntax.Parser.Monad |
| parseFile' | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseFlags | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad |
| 2 (Data Constructor) | Agda.Syntax.Parser.Monad |
| parseFlags | Agda.Syntax.Parser.Monad |
| parseInp | Agda.Syntax.Parser.Monad |
| parseKeepComments | Agda.Syntax.Parser.Monad |
| parseLastPos | Agda.Syntax.Parser.Monad |
| parseLayout | Agda.Syntax.Parser.Monad |
| parseLexState | Agda.Syntax.Parser.Monad |
| parseLHS | Agda.Syntax.Concrete.Operators |
| parseLiterate | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseOk | Agda.Syntax.Parser.Monad |
| parsePluginOptions | Agda.Interaction.Options |
| parsePos | Agda.Syntax.Parser.Monad |
| parsePosString | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| parsePragmaOptions | Agda.Interaction.Options |
| parsePrevChar | Agda.Syntax.Parser.Monad |
| parsePrevToken | Agda.Syntax.Parser.Monad |
| Parser | |
| 1 (Type/Class) | Agda.Syntax.Parser.Monad |
| 2 (Type/Class) | Agda.Syntax.Parser, Agda.Interaction.GhciTop |
| ParseResult | Agda.Syntax.Parser.Monad |
| parseStandardOptions | Agda.Interaction.Options |
| ParseState | Agda.Syntax.Parser.Monad |
| partP | Agda.Syntax.Concrete.Operators.Parser |
| Pat | Agda.Auto.Syntax |
| PatConApp | Agda.Auto.Syntax |
| PatExp | Agda.Auto.Syntax |
| PatInfo | Agda.Syntax.Info |
| PatName | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| PatRange | Agda.Syntax.Info |
| PatSource | Agda.Syntax.Info |
| patsToTerms | Agda.TypeChecking.With |
| Pattern | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Type/Class) | Agda.Syntax.Internal |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| Pattern' | Agda.Syntax.Abstract |
| PatternErr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatternShadowsConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| patternViolation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PatVar | Agda.Auto.Syntax |
| PB | Agda.Auto.NarrowingSearch |
| PBlocked | Agda.Auto.NarrowingSearch |
| pconName | Agda.Compiler.MAlonzo.Primitives |
| PDoubleBlocked | Agda.Auto.NarrowingSearch |
| PEConApp | Agda.Auto.Typecheck |
| PENo | Agda.Auto.Typecheck |
| performKill | Agda.TypeChecking.MetaVars.Occurs |
| Perm | Agda.Utils.Permutation |
| Permutation | Agda.Utils.Permutation |
| permute | Agda.Utils.Permutation |
| PEval | Agda.Auto.Typecheck |
| pfail | Agda.Utils.ReadP |
| pHidden | Agda.Syntax.Concrete.Pretty |
| Pi | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| piAbstractTerm | Agda.TypeChecking.Abstract |
| piApply | Agda.TypeChecking.Substitute |
| piApplyM | Agda.TypeChecking.Telescope |
| piBrackets | Agda.Syntax.Fixity |
| pickid | Agda.Auto.Typecheck |
| piFreq | Agda.TypeChecking.Test.Generators |
| PiHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| plugHole | Agda.Syntax.Internal.Pattern |
| Plus | Agda.TypeChecking.Level |
| PlusView | Agda.TypeChecking.Level |
| Pn | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| polarities | Agda.TypeChecking.Polarity |
| Polarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| polarity | Agda.TypeChecking.Polarity |
| popContext | Agda.Syntax.Parser.Monad |
| popLexState | Agda.Syntax.Parser.Monad |
| popMapS | Agda.Auto.Convert |
| posCol | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Position | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| positionInvariant | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| Positive | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| positive | Agda.Utils.TestHelpers |
| positivityCheckEnabled | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| posLine | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| posPos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| postfixP | Agda.Syntax.Concrete.Operators.Parser |
| postop | Agda.Syntax.Concrete.Operators.Parser |
| posToRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| PostponedTypeCheckingProblem | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| postponeTypeCheckingProblem | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| postponeTypeCheckingProblem_ | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| Postulate | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| Pragma | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| PragmaOptions | |
| 1 (Type/Class) | Agda.Interaction.Options |
| 2 (Data Constructor) | Agda.Interaction.Options |
| pragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Precedence | Agda.Syntax.Fixity |
| Pred | Agda.TypeChecking.Primitive |
| Prefix | Agda.Utils.List |
| PrefixDef | Agda.Syntax.Common |
| prefixP | Agda.Syntax.Concrete.Operators.Parser |
| pRelevance | Agda.Syntax.Concrete.Pretty |
| preMeta | Agda.Interaction.GhciTop |
| preop | Agda.Syntax.Concrete.Operators.Parser |
| preserveDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| Pretty | Agda.Utils.Pretty |
| pretty | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyA | |
| 1 (Function) | Agda.Syntax.Abstract.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| prettyATop | Agda.Syntax.Abstract.Pretty |
| prettyBehaviour | Agda.Termination.CallGraph |
| PrettyContext | |
| 1 (Type/Class) | Agda.TypeChecking.Pretty |
| 2 (Data Constructor) | Agda.TypeChecking.Pretty |
| prettyContext | Agda.Interaction.GhciTop |
| prettyEpicFun | Agda.Compiler.Epic.Epic |
| prettyError | Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyGraph | Agda.TypeChecking.Positivity |
| prettyList | Agda.TypeChecking.Pretty |
| prettyPrec | Agda.Utils.Pretty |
| prettyPrint | Agda.Compiler.MAlonzo.Pretty |
| PrettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyTCM | Agda.TypeChecking.Pretty, Agda.TypeChecking.Errors, Agda.Interaction.GhciTop |
| prettyTypeOfMeta | Agda.Interaction.GhciTop |
| preUscore | Agda.Interaction.GhciTop |
| PreviousInput | Agda.Syntax.Parser.Alex |
| Prim | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primAgdaTerm | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermCon | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermDef | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermLam | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermPi | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermSort | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermUnsupported | Agda.TypeChecking.Monad.Builtin |
| primAgdaTermVar | Agda.TypeChecking.Monad.Builtin |
| primArg | Agda.TypeChecking.Monad.Builtin |
| primArgArg | Agda.TypeChecking.Monad.Builtin |
| primBody | Agda.Compiler.MAlonzo.Primitives |
| primBool | Agda.TypeChecking.Monad.Builtin |
| primChar | Agda.TypeChecking.Monad.Builtin |
| primClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primCompiled | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primCons | Agda.TypeChecking.Monad.Builtin |
| Prime | Agda.Utils.Suffix |
| primEquality | Agda.TypeChecking.Monad.Builtin |
| primExpr | Agda.Compiler.Epic.Primitive |
| primFalse | Agda.TypeChecking.Monad.Builtin |
| primFlat | Agda.TypeChecking.Monad.Builtin |
| primFloat | Agda.TypeChecking.Monad.Builtin |
| PrimFun | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFun | Agda.Compiler.Epic.Primitive |
| primFunArity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunImplementation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primFunName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PrimImpl | Agda.TypeChecking.Primitive |
| primInf | Agda.TypeChecking.Monad.Builtin |
| primInteger | Agda.TypeChecking.Monad.Builtin |
| primIO | Agda.TypeChecking.Monad.Builtin |
| Primitive | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| 3 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 4 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| PrimitiveFunction | Agda.Syntax.Concrete.Definitions |
| primitiveFunctions | Agda.TypeChecking.Primitive |
| PrimitiveImpl | Agda.TypeChecking.Primitive |
| PrimitiveType | Agda.Interaction.Highlighting.Precise |
| primitivise | Agda.Compiler.Epic.Primitive |
| primLevel | Agda.TypeChecking.Monad.Builtin |
| primLevelMax | Agda.TypeChecking.Monad.Builtin |
| primLevelSuc | Agda.TypeChecking.Monad.Builtin |
| primLevelZero | Agda.TypeChecking.Monad.Builtin |
| primList | Agda.TypeChecking.Monad.Builtin |
| primLists | Agda.Compiler.Epic.Primitive |
| primName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| primNat | Agda.TypeChecking.Monad.Builtin |
| primNatCaseZD | Agda.Compiler.Epic.Primitive |
| primNatCaseZS | Agda.Compiler.Epic.Primitive |
| primNatDivSucAux | Agda.TypeChecking.Monad.Builtin |
| primNatEquality | Agda.TypeChecking.Monad.Builtin |
| primNatLess | Agda.TypeChecking.Monad.Builtin |
| primNatMinus | Agda.TypeChecking.Monad.Builtin |
| primNatModSucAux | Agda.TypeChecking.Monad.Builtin |
| primNatPlus | Agda.TypeChecking.Monad.Builtin |
| primNatTimes | Agda.TypeChecking.Monad.Builtin |
| primNil | Agda.TypeChecking.Monad.Builtin |
| primQName | Agda.TypeChecking.Monad.Builtin |
| primRefl | Agda.TypeChecking.Monad.Builtin |
| primSharp | Agda.TypeChecking.Monad.Builtin |
| primSize | Agda.TypeChecking.Monad.Builtin |
| primSizeInf | Agda.TypeChecking.Monad.Builtin |
| primSizeSuc | Agda.TypeChecking.Monad.Builtin |
| primString | Agda.TypeChecking.Monad.Builtin |
| primSuc | Agda.TypeChecking.Monad.Builtin |
| PrimTerm | Agda.TypeChecking.Primitive |
| primTerm | Agda.TypeChecking.Primitive |
| PrimTF | Agda.Compiler.Epic.Primitive |
| PrimTransform | Agda.Compiler.Epic.Primitive |
| primTrue | Agda.TypeChecking.Monad.Builtin |
| primTrustMe | Agda.TypeChecking.Primitive |
| PrimType | Agda.TypeChecking.Primitive |
| primType | Agda.TypeChecking.Primitive |
| primZero | Agda.TypeChecking.Monad.Builtin |
| print | Agda.Utils.IO.Locale |
| printTestCase | Agda.Utils.QuickCheck |
| printUsage | Agda.Main |
| printVersion | Agda.Main |
| Prio | Agda.Auto.NarrowingSearch |
| prioAbsurdLambda | Agda.Auto.SearchControl |
| prioCompareArgList | Agda.Auto.SearchControl |
| prioCompBeta | Agda.Auto.SearchControl |
| prioCompBetaStructured | Agda.Auto.SearchControl |
| prioCompChoice | Agda.Auto.SearchControl |
| prioCompCopy | Agda.Auto.SearchControl |
| prioCompIota | Agda.Auto.SearchControl |
| prioCompUnif | Agda.Auto.SearchControl |
| prioInferredTypeUnknown | Agda.Auto.SearchControl |
| PrioMeta | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| prioNo | Agda.Auto.SearchControl |
| prioNoIota | Agda.Auto.SearchControl |
| prioProjIndex | Agda.Auto.SearchControl |
| prioTypecheck | Agda.Auto.SearchControl |
| prioTypecheckArgList | Agda.Auto.SearchControl |
| prioTypeUnknown | Agda.Auto.SearchControl |
| Private | Agda.Syntax.Concrete |
| PrivateAccess | Agda.Syntax.Common |
| PrivateNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Problem | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Data Constructor) | Agda.TypeChecking.Rules.LHS.Problem |
| Problem' | Agda.TypeChecking.Rules.LHS.Problem |
| problemInPat | Agda.TypeChecking.Rules.LHS.Problem |
| problemOutPat | Agda.TypeChecking.Rules.LHS.Problem |
| ProblemPart | Agda.TypeChecking.Rules.LHS.Problem |
| problemTel | Agda.TypeChecking.Rules.LHS.Problem |
| ProjectRoot | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| projectRoot | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| promote | Agda.Utils.QuickCheck |
| proofIrrelevance | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Prop | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Auto.NarrowingSearch |
| 3 (Data Constructor) | Agda.Syntax.Concrete |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| prop | Agda.Syntax.Internal |
| propagatePrio | Agda.Auto.NarrowingSearch |
| Property | Agda.Utils.QuickCheck |
| property | Agda.Utils.QuickCheck |
| propFreq | Agda.TypeChecking.Test.Generators |
| PropMustBeSingleton | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| prop_disjoint | Agda.Utils.Warshall |
| prop_distinct_fastDistinct | Agda.Utils.List |
| prop_extractNthElement | Agda.Utils.List |
| prop_flattenTelInv | Agda.TypeChecking.Tests |
| prop_flattenTelScope | Agda.TypeChecking.Tests |
| prop_genericElemIndex | Agda.Utils.List |
| prop_groupBy' | Agda.Utils.List |
| prop_path | Agda.Utils.Warshall |
| prop_reorderTelStable | Agda.TypeChecking.Tests |
| prop_smaller | Agda.Utils.Warshall |
| prop_splitTelescopePermScope | Agda.TypeChecking.Tests |
| prop_splitTelescopeScope | Agda.TypeChecking.Tests |
| prop_stable | Agda.Utils.Warshall |
| prop_telToListInv | Agda.TypeChecking.Tests |
| prop_wellScopedVars | Agda.TypeChecking.Test.Generators |
| PState | Agda.Syntax.Parser.Monad |
| PStr | Agda.Utils.Pretty |
| ptext | Agda.Utils.Pretty |
| Ptr | Agda.Utils.Pointer |
| PublicAccess | Agda.Syntax.Common |
| publicModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| PublicNS | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| publicOpen | Agda.Syntax.Concrete |
| punctuate | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| pureTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| pushContext | Agda.Syntax.Parser.Monad |
| pushCurrentContext | Agda.Syntax.Parser.Monad |
| pushLexState | Agda.Syntax.Parser.Monad |
| putConPar | Agda.Compiler.Epic.CompileState |
| putDelayed | Agda.Compiler.Epic.CompileState |
| putIrrFilter | Agda.Compiler.Epic.CompileState |
| putMain | Agda.Compiler.Epic.CompileState |
| putStr | Agda.Utils.IO.Locale |
| putStrLn | Agda.Utils.IO.Locale |
| pwords | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| Q | Agda.Interaction.GhciTop |
| QName | |
| 1 (Type/Class) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| 4 (Data Constructor) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameFromList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameModule | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameParts | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| qnameToConcrete | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameToList | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qnameToMName | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qNameType | Agda.TypeChecking.Quote |
| QPB | Agda.Auto.NarrowingSearch |
| QPBlocked | Agda.Auto.NarrowingSearch |
| QPDoubleBlocked | Agda.Auto.NarrowingSearch |
| Qual | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| qualify | |
| 1 (Function) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Function) | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qualifyM | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| qualifyQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| QuestionMark | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| quickCheck | Agda.Utils.QuickCheck |
| quickCheck' | Agda.Utils.QuickCheck |
| quickCheckResult | Agda.Utils.QuickCheck |
| quickCheckWith | Agda.Utils.QuickCheck |
| quickCheckWith' | Agda.Utils.QuickCheck |
| quickCheckWithResult | Agda.Utils.QuickCheck |
| Quote | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| quote | Agda.Utils.String |
| QuoteGoal | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| quoteName | Agda.TypeChecking.Quote |
| quotes | Agda.Utils.Pretty |
| quoteTerm | Agda.TypeChecking.Quote |
| quoteType | Agda.TypeChecking.Quote |
| R | Agda.Utils.Map |
| Raise | Agda.TypeChecking.Substitute |
| raise | Agda.TypeChecking.Substitute |
| raiseFrom | Agda.TypeChecking.Substitute |
| raiseFromCC | Agda.Compiler.Epic.Forcing |
| Range | |
| 1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 3 (Type/Class) | Agda.Interaction.Highlighting.Range |
| 4 (Data Constructor) | Agda.Interaction.Highlighting.Range |
| RangeAndPragma | |
| 1 (Type/Class) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| rangeInvariant | |
| 1 (Function) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Function) | Agda.Interaction.Highlighting.Range |
| ranges | Agda.Utils.QuickCheck |
| rangeToInterval | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| rational | Agda.Utils.Pretty |
| RawApp | Agda.Syntax.Concrete |
| RawAppP | Agda.Syntax.Concrete |
| RB | Agda.Termination.Lexicographic |
| rbrace | Agda.Utils.Pretty |
| rbrack | Agda.Utils.Pretty |
| RConst | Agda.Utils.Warshall |
| readBinaryFile' | Agda.Utils.IO.Binary |
| readInterface | Agda.Interaction.Imports |
| readline | Agda.Interaction.Monad |
| readM | Agda.Utils.Monad |
| ReadP | Agda.Utils.ReadP |
| readTextFile | Agda.Utils.IO.UTF8 |
| reason | Agda.Utils.QuickCheck |
| rebindClause | Agda.TypeChecking.Rebind |
| rebindPrimitive | Agda.TypeChecking.Primitive |
| rebuild | Agda.Syntax.Concrete.Operators.Parser |
| rebuildBinding | Agda.Syntax.Concrete.Operators.Parser |
| Rec | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| recAbstr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recalc | Agda.Auto.NarrowingSearch |
| recalcs | Agda.Auto.NarrowingSearch |
| recArgOccurrences | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| RecBehaviour | Agda.Termination.Lexicographic |
| recBehaviourInvariant | Agda.Termination.Lexicographic |
| reccalc | Agda.Auto.NarrowingSearch |
| recClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recConType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| RecDef | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Data Constructor) | Agda.Syntax.Concrete.Definitions |
| recEtaEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recFields | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recNamedCon | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Record | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recordModule | Agda.TypeChecking.Records |
| Records | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| recPars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recPolarity | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recTel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| recursive | Agda.Syntax.Concrete.Operators.Parser |
| redBind | Agda.TypeChecking.Primitive |
| redReturn | Agda.TypeChecking.Primitive |
| Reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduce | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduceB | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| reduceCon | Agda.TypeChecking.Rules.Term |
| Reduced | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| reduced | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| reduceHead | Agda.TypeChecking.Injectivity |
| RefCreateEnv | Agda.Auto.NarrowingSearch |
| Refinable | Agda.Auto.NarrowingSearch |
| refine | Agda.Interaction.BasicOps |
| refinements | Agda.Auto.NarrowingSearch |
| refineMeta | Agda.Interaction.CommandLine.CommandLine |
| RefInfo | Agda.Auto.Syntax |
| refreshStr | Agda.Interaction.GhciTop |
| Reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reify | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyApp | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyDisplayForm | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyDisplayFormP | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| reifyPatterns | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| Rel | |
| 1 (Data Constructor) | Agda.Compiler.Epic.Erasure |
| 2 (Type/Class) | Agda.TypeChecking.Primitive |
| RelativeTo | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Relevance | Agda.Syntax.Common |
| relevancies | Agda.Compiler.Epic.Erasure |
| Relevancy | Agda.Compiler.Epic.Erasure |
| Relevant | Agda.Syntax.Common |
| relevant | Agda.Compiler.Epic.Erasure |
| relOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| remForced | Agda.Compiler.Epic.Forcing |
| removeForced | Agda.Compiler.Epic.Forcing |
| removeInteractionPoint | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| removevar | Agda.Auto.CaseSplit |
| Ren | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| ren | Agda.Auto.CaseSplit |
| rename | |
| 1 (Function) | Agda.Auto.CaseSplit |
| 2 (Function) | Agda.TypeChecking.Telescope |
| renameCanonicalNames | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| renamep | Agda.Auto.CaseSplit |
| Renaming | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| renaming | |
| 1 (Function) | Agda.Syntax.Concrete |
| 2 (Function) | Agda.TypeChecking.Telescope |
| renamingR | Agda.TypeChecking.Telescope |
| rEnd | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| render | Agda.Utils.Pretty |
| renderStyle | Agda.Utils.Pretty |
| renFrom | Agda.Syntax.Concrete |
| renTo | Agda.Syntax.Concrete |
| renToRange | Agda.Syntax.Concrete |
| reorderTel | Agda.TypeChecking.Telescope |
| RepeatedVariablesInPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| repl | Agda.Compiler.MAlonzo.Primitives |
| replace | Agda.Auto.CaseSplit |
| replaceAt | Agda.Compiler.Epic.CompileState |
| replaceForced | Agda.Compiler.Epic.Forcing |
| replacep | Agda.Auto.CaseSplit |
| replay | Agda.Utils.QuickCheck |
| reportS | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| reportSDoc | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| reportSLn | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| requireLevels | Agda.TypeChecking.Level |
| resetState | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| resize | Agda.Utils.QuickCheck |
| resizeConf | Agda.TypeChecking.Test.Generators |
| ResolvedName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| resolveModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| resolveName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| response | Agda.Interaction.GhciTop |
| Restore | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| restrictPrivate | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| Result | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Termination.TermCheck |
| retryConstraints | Agda.Interaction.CommandLine.CommandLine |
| Return | Agda.Interaction.CommandLine.CommandLine |
| reverseCCBody | Agda.Compiler.Epic.FromAgda |
| reverseP | Agda.Utils.Permutation |
| Rewrite | Agda.Interaction.BasicOps |
| rewrite | Agda.Interaction.BasicOps |
| RewriteRHS | Agda.Syntax.Abstract |
| RHS | |
| 1 (Type/Class) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Type/Class) | Agda.Syntax.Abstract |
| 4 (Data Constructor) | Agda.Syntax.Abstract |
| ribbonsPerLine | Agda.Utils.Pretty |
| RICheckElim | Agda.Auto.Syntax |
| RICheckProjIndex | Agda.Auto.Syntax |
| RICopyInfo | Agda.Auto.Syntax |
| rieDefFreeVars | Agda.Auto.Syntax |
| rieEqReasoningConsts | Agda.Auto.Syntax |
| rieHints | Agda.Auto.Syntax |
| RIEnv | Agda.Auto.Syntax |
| RIEqRState | Agda.Auto.Syntax |
| RightAssoc | Agda.Syntax.Fixity |
| RightDisjunct | Agda.Auto.NarrowingSearch |
| rightDistributive | Agda.Utils.TestHelpers |
| RightHandSide | Agda.Syntax.Translation.ConcreteToAbstract, Agda.Interaction.GhciTop |
| RightOperandCtx | Agda.Syntax.Fixity |
| Rigid | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Data Constructor) | Agda.Utils.Warshall |
| 3 (Data Constructor) | Agda.TypeChecking.MetaVars.Occurs |
| 4 (Data Constructor) | Agda.TypeChecking.SizedTypes |
| RigidId | Agda.Utils.Warshall |
| rigidVars | Agda.TypeChecking.Free |
| RIInferredTypeUnknown | Agda.Auto.Syntax |
| RIIotaStep | Agda.Auto.Syntax |
| RIMainInfo | Agda.Auto.Syntax |
| RINotConstructor | Agda.Auto.Syntax |
| RIPickSubsvar | Agda.Auto.Syntax |
| RIUnifInfo | Agda.Auto.Syntax |
| RIUsedVars | Agda.Auto.Syntax |
| rm | Agda.Auto.CaseSplit |
| rollback | Agda.Syntax.Parser.LookAhead |
| roundFixBrackets | Agda.Syntax.Fixity |
| row | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| rowdescr | Agda.Utils.Warshall |
| rows | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| rparen | Agda.Utils.Pretty |
| rStart | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| rteModule | Agda.Compiler.MAlonzo.Compiler |
| rtmError | Agda.Compiler.MAlonzo.Misc |
| rtmMod | Agda.Compiler.MAlonzo.Misc |
| rtmQual | Agda.Compiler.MAlonzo.Misc |
| rtmVar | Agda.Compiler.MAlonzo.Misc |
| rToR | Agda.Interaction.Highlighting.Range |
| runAbsToCon | Agda.Syntax.Translation.AbstractToConcrete, Agda.Interaction.GhciTop |
| runAgda | Agda.Main |
| runExceptionT | Agda.TypeChecking.Monad.Exception |
| runIM | Agda.Interaction.Monad |
| runLookAhead | Agda.Syntax.Parser.LookAhead |
| runNice | Agda.Syntax.Concrete.Definitions |
| runTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| runTCM' | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| runTests | Agda.Utils.TestHelpers |
| runUndo | Agda.Auto.NarrowingSearch |
| RVar | Agda.Utils.Warshall |
| S | |
| 1 (Type/Class) | Agda.Auto.Convert |
| 2 (Data Constructor) | Agda.Auto.Convert |
| sameVars | Agda.TypeChecking.Conversion |
| sample | Agda.Utils.QuickCheck |
| sample' | Agda.Utils.QuickCheck |
| satisfy | Agda.Utils.ReadP |
| sccomcount | Agda.Auto.NarrowingSearch |
| scflip | Agda.Auto.NarrowingSearch |
| sChecked | Agda.Interaction.GhciTop |
| SClause | Agda.TypeChecking.Coverage |
| sConsts | Agda.Auto.Convert |
| Scope | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 3 (Type/Class) | Agda.Utils.Warshall |
| ScopeCheckDeclaration | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ScopeCheckDefinition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ScopeCheckExpr | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| scopeCheckImport | Agda.Interaction.Imports |
| ScopeCheckLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| scopeCurrent | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ScopedDecl | Agda.Syntax.Abstract |
| ScopedDef | Agda.Syntax.Abstract |
| ScopedExpr | Agda.Syntax.Abstract |
| scopeImported | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeImports | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ScopeInfo | |
| 1 (Type/Class) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeLocals | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeLookup | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| ScopeM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| scopeModules | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeName | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopeParents | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopePrecedence | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopePrivate | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scopePublic | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| scPats | Agda.TypeChecking.Coverage |
| scPerm | Agda.TypeChecking.Coverage |
| scsub1 | Agda.Auto.NarrowingSearch |
| scsub2 | Agda.Auto.NarrowingSearch |
| scSubst | Agda.TypeChecking.Coverage |
| scTel | Agda.TypeChecking.Coverage |
| sCurMeta | Agda.Auto.Convert |
| secFreeVars | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| secondPart | Agda.TypeChecking.Telescope |
| secTelescope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Section | |
| 1 (Data Constructor) | Agda.Syntax.Abstract |
| 2 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 3 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Sections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| semi | Agda.Utils.Pretty |
| SemiRing | |
| 1 (Type/Class) | Agda.Utils.SemiRing |
| 2 (Type/Class) | Agda.Termination.Semiring |
| Semiring | |
| 1 (Type/Class) | Agda.Termination.Semiring |
| 2 (Data Constructor) | Agda.Termination.Semiring |
| semiringInvariant | Agda.Termination.Semiring |
| sep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| sepBy | Agda.Utils.ReadP |
| sepBy1 | Agda.Utils.ReadP |
| seqc | Agda.Auto.NarrowingSearch |
| seqctx | Agda.Auto.CaseSplit |
| sEqs | Agda.Auto.Convert |
| Set | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| set | Agda.Syntax.Internal |
| set0 | Agda.Syntax.Internal |
| setArgOccurrences | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setBuiltinThings | Agda.TypeChecking.Monad.Builtin |
| setCommandLineOptions | |
| 1 (Function) | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Interaction.GhciTop |
| setContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| setCurrentModule | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| setCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad |
| setDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| setFreqs | Agda.TypeChecking.Test.Generators |
| setImportedSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setInput | Agda.Syntax.Parser.LookAhead |
| setInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setInterface | Agda.Compiler.MAlonzo.Misc |
| setLastPos | Agda.Syntax.Parser.Monad |
| setLexInput | Agda.Syntax.Parser.Alex |
| setLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| setMutualBlock | Agda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad |
| SetN | Agda.Syntax.Concrete |
| setOptionsFromPragma | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setParsePos | Agda.Syntax.Parser.Monad |
| setPolarity | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setPragmaOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setPrevToken | Agda.Syntax.Parser.Monad |
| SetRange | |
| 1 (Type/Class) | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| setRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| setScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setScopeAccess | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| setShowImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| setSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| setTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| setVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| several | Agda.Interaction.Highlighting.Precise |
| ShadowedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeApplicationOf | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeAppliedToTheDatatypeParameters | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeASort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeEmpty | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBePi | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldBeRecordType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| ShouldEndInApplicationOfTheDatatype | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| shouldEtaContractImplicit | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| shouldReifyInteractionPoints | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| showA | Agda.Syntax.Abstract.Pretty |
| showATop | Agda.Syntax.Abstract.Pretty |
| showChar' | Agda.Syntax.Concrete.Pretty |
| showComparison | Agda.Interaction.BasicOps |
| showConstraints | Agda.Interaction.CommandLine.CommandLine |
| showContext | Agda.Interaction.CommandLine.CommandLine |
| showHighlightingInfo | Agda.Interaction.Highlighting.Emacs |
| showImplicitArgs | Agda.Interaction.GhciTop |
| showImplicitArguments | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| showIndex | Agda.Utils.String |
| showMetas | Agda.Interaction.CommandLine.CommandLine |
| showModuleContents | Agda.Interaction.GhciTop |
| showNumIId | Agda.Interaction.GhciTop |
| showPat | Agda.TypeChecking.With |
| showQNameId | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| showScope | Agda.Interaction.CommandLine.CommandLine |
| showStatus | Agda.Interaction.GhciTop |
| showString' | Agda.Syntax.Concrete.Pretty |
| shrink | Agda.Utils.QuickCheck |
| Shrink2 | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| ShrinkC | Agda.TypeChecking.Test.Generators |
| shrinkC | Agda.TypeChecking.Test.Generators |
| Shrinking | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| shrinking | Agda.Utils.QuickCheck |
| shrinkInit | Agda.Utils.QuickCheck |
| shrinkIntegral | Agda.Utils.QuickCheck |
| shrinkNothing | Agda.Utils.QuickCheck |
| shrinkRealFrac | Agda.Utils.QuickCheck |
| ShrinkState | Agda.Utils.QuickCheck |
| shrinkState | Agda.Utils.QuickCheck |
| Sidecondition | Agda.Auto.NarrowingSearch |
| Sig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigDefinitions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigMName | Agda.Compiler.MAlonzo.Misc |
| Signature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sigSections | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| singleConstructorType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| singleton | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Interaction.Highlighting.Precise |
| SingletonRecords | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| Size | |
| 1 (Type/Class) | Agda.Termination.SparseMatrix |
| 2 (Data Constructor) | Agda.Termination.SparseMatrix |
| 3 (Type/Class) | Agda.Termination.Matrix |
| 4 (Data Constructor) | Agda.Termination.Matrix |
| size | |
| 1 (Function) | Agda.Utils.Size |
| 2 (Function) | Agda.Termination.SparseMatrix |
| 3 (Function) | Agda.Termination.Matrix |
| 4 (Function) | Agda.Termination.Lexicographic |
| SizeConst | Agda.Utils.Warshall |
| SizeConstraint | Agda.TypeChecking.SizedTypes |
| Sized | Agda.Utils.Size |
| sized | Agda.Utils.QuickCheck |
| SizedList | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| SizeExpr | |
| 1 (Type/Class) | Agda.Utils.Warshall |
| 2 (Type/Class) | Agda.TypeChecking.SizedTypes |
| sizeExpr | Agda.TypeChecking.SizedTypes |
| SizeInf | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeInvariant | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| SizeMeta | Agda.TypeChecking.SizedTypes |
| sizePolarity | Agda.TypeChecking.Polarity |
| sizeRigid | Agda.Utils.Warshall |
| SizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeSuc | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeType | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| SizeVar | Agda.Utils.Warshall |
| SizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| sizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| Skip | Agda.Auto.Syntax |
| skipBlock | Agda.Syntax.Parser.Comments |
| skipMany | Agda.Utils.ReadP |
| skipMany1 | Agda.Utils.ReadP |
| skipSpaces | Agda.Utils.ReadP |
| sLub | Agda.Syntax.Internal |
| sMainMeta | Agda.Auto.Convert |
| smallestPos | Agda.Interaction.Highlighting.Precise |
| Smart | |
| 1 (Data Constructor) | Agda.Utils.QuickCheck |
| 2 (Type/Class) | Agda.Utils.QuickCheck |
| smashTel | Agda.Syntax.Concrete.Pretty |
| sMetas | Agda.Auto.Convert |
| Sol | Agda.Auto.CaseSplit |
| Solution | Agda.Utils.Warshall |
| solve | Agda.Utils.Warshall |
| solveConstraint | Agda.TypeChecking.Constraints |
| solveConstraints | Agda.TypeChecking.Constraints |
| solveLevelConstraints | Agda.TypeChecking.UniversePolymorphism |
| solveSizeConstraints | Agda.TypeChecking.SizedTypes |
| SomeWhere | Agda.Syntax.Concrete |
| Sort | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.Auto.Syntax |
| 3 (Type/Class) | Agda.Syntax.Internal |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| sort | Agda.Syntax.Internal |
| SortCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sortFreq | Agda.TypeChecking.Test.Generators |
| SortFreqs | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| sortFreqs | Agda.TypeChecking.Test.Generators |
| SortHead | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| sortInteractionPoints | Agda.Interaction.GhciTop |
| sortOfConst | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| source | Agda.Termination.CallGraph |
| SourceToModule | Agda.Interaction.FindFile |
| sourceToModule | Agda.Interaction.FindFile |
| space | Agda.Utils.Pretty |
| splashScreen | Agda.Interaction.CommandLine.CommandLine |
| Split | Agda.TypeChecking.Rules.LHS.Problem |
| split | Agda.TypeChecking.Coverage |
| split' | Agda.TypeChecking.Coverage |
| splitC | Agda.TypeChecking.CompiledClause |
| SplitClause | Agda.TypeChecking.Coverage |
| splitClause | Agda.TypeChecking.Coverage |
| splitClauseWithAbs | Agda.TypeChecking.Coverage |
| SplitError | |
| 1 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| 2 (Type/Class) | Agda.TypeChecking.Coverage |
| splitOn | Agda.TypeChecking.CompiledClause |
| SplitOnIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| SplitPanic | Agda.TypeChecking.Rules.LHS.Problem |
| splitPerm | Agda.TypeChecking.Telescope |
| SplitProblem | Agda.TypeChecking.Rules.LHS.Problem |
| splitProblem | Agda.TypeChecking.Rules.LHS.Split |
| SplitTel | |
| 1 (Type/Class) | Agda.TypeChecking.Telescope |
| 2 (Data Constructor) | Agda.TypeChecking.Telescope |
| splitTelescope | Agda.TypeChecking.Telescope |
| square | |
| 1 (Function) | Agda.Termination.SparseMatrix |
| 2 (Function) | Agda.Termination.Matrix |
| srcFile | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| SRes | Agda.Auto.NarrowingSearch |
| sShowImplicitArguments | Agda.Interaction.GhciTop |
| sSuc | Agda.Syntax.Internal |
| Stack | Agda.TypeChecking.CompiledClause.Match |
| standardOptions_ | Agda.Interaction.Options |
| startPos | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| State | |
| 1 (Type/Class) | Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Interaction.GhciTop |
| Statistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Status | |
| 1 (Type/Class) | Agda.Interaction.GhciTop |
| 2 (Data Constructor) | Agda.Interaction.GhciTop |
| status | Agda.Interaction.GhciTop |
| stBuiltinThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stCurrentModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stdArgs | Agda.Utils.QuickCheck |
| stDecodedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stdoutFlush | Agda.Utils.IO.Locale |
| step | Agda.Compiler.Epic.Erasure |
| stFreshThings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stHaskellImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImportedBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImportedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stImports | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stInteractionPoints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stLocalBuiltins | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stMetaStore | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stModuleToSource | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stMutualBlocks | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| store | Agda.Utils.Pointer |
| storeDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| stPersistentOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stPragmaOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Str | |
| 1 (Type/Class) | Agda.Utils.QuickCheck |
| 2 (Data Constructor) | Agda.Utils.Pretty |
| 3 (Type/Class) | Agda.TypeChecking.Primitive |
| 4 (Data Constructor) | Agda.TypeChecking.Primitive |
| Strict | Agda.Syntax.Strict |
| strict | Agda.Syntax.Strict |
| String | Agda.Interaction.Highlighting.Precise |
| string | Agda.Utils.ReadP |
| stripImplicits | Agda.Syntax.Translation.InternalToAbstract, Agda.Interaction.GhciTop |
| stripNoNames | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| stripWithClausePatterns | Agda.TypeChecking.With |
| stScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stSignature | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stStatistics | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| stVisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Style | |
| 1 (Type/Class) | Agda.Utils.Pretty |
| 2 (Data Constructor) | Agda.Utils.Pretty |
| style | Agda.Utils.Pretty |
| Sub | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Unify |
| sub | Agda.Auto.Syntax |
| SubConstraints | |
| 1 (Type/Class) | Agda.Auto.NarrowingSearch |
| 2 (Data Constructor) | Agda.Auto.NarrowingSearch |
| subi | Agda.Auto.Syntax |
| Subst | Agda.TypeChecking.Substitute |
| subst | |
| 1 (Function) | Agda.Compiler.Epic.AuxAST |
| 2 (Function) | Agda.TypeChecking.Substitute |
| substBranch | Agda.Compiler.Epic.AuxAST |
| substCC | Agda.Compiler.Epic.Forcing |
| substCCBody | Agda.Compiler.Epic.Forcing |
| Substitution | |
| 1 (Type/Class) | Agda.TypeChecking.Substitute |
| 2 (Type/Class) | Agda.TypeChecking.Rules.LHS.Problem |
| substLit | Agda.Compiler.Epic.FromAgda |
| substs | Agda.TypeChecking.Substitute |
| substsCCBody | Agda.Compiler.Epic.Forcing |
| substTerm | Agda.Compiler.Epic.FromAgda |
| substUnder | Agda.TypeChecking.Substitute |
| subsvars | Agda.Auto.SearchControl |
| Suc | Agda.Syntax.Internal |
| Success | Agda.Utils.QuickCheck |
| suchThat | Agda.Utils.QuickCheck |
| suchThatMaybe | Agda.Utils.QuickCheck |
| sucName | Agda.TypeChecking.Level |
| Suffix | |
| 1 (Type/Class) | Agda.Utils.Suffix |
| 2 (Type/Class) | Agda.Utils.List |
| suffixView | Agda.Utils.Suffix |
| supremum | Agda.Termination.CallGraph |
| SymArrow | Agda.Syntax.Parser.Tokens |
| SymAs | Agda.Syntax.Parser.Tokens |
| SymBar | Agda.Syntax.Parser.Tokens |
| Symbol | |
| 1 (Type/Class) | Agda.Syntax.Parser.Tokens |
| 2 (Data Constructor) | Agda.Interaction.Highlighting.Precise |
| symbol | Agda.Syntax.Parser.LexActions |
| SymCloseBrace | Agda.Syntax.Parser.Tokens |
| SymCloseParen | Agda.Syntax.Parser.Tokens |
| SymClosePragma | Agda.Syntax.Parser.Tokens |
| SymCloseVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymColon | Agda.Syntax.Parser.Tokens |
| SymDot | Agda.Syntax.Parser.Tokens |
| SymEllipsis | Agda.Syntax.Parser.Tokens |
| SymEqual | Agda.Syntax.Parser.Tokens |
| SymLambda | Agda.Syntax.Parser.Tokens |
| SymOpenBrace | Agda.Syntax.Parser.Tokens |
| SymOpenParen | Agda.Syntax.Parser.Tokens |
| SymOpenPragma | Agda.Syntax.Parser.Tokens |
| SymOpenVirtualBrace | Agda.Syntax.Parser.Tokens |
| SymQuestionMark | Agda.Syntax.Parser.Tokens |
| SymSemi | Agda.Syntax.Parser.Tokens |
| SymUnderscore | Agda.Syntax.Parser.Tokens |
| SymVirtualSemi | Agda.Syntax.Parser.Tokens |
| sync | Agda.Syntax.Parser.LookAhead |
| Syntax | Agda.Syntax.Concrete |
| syntaxOf | Agda.Syntax.Fixity |
| 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 |
| U | Agda.TypeChecking.Rules.LHS.Unify |
| UId | Agda.Auto.Syntax |
| umodifyIORef | Agda.Auto.NarrowingSearch |
| unAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| unAppView | Agda.Syntax.Abstract.Views |
| unArg | Agda.Syntax.Common |
| UnBlock | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unblockedTester | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| unConName | Agda.TypeChecking.Test.Generators |
| uncurry3 | Agda.Utils.Tuple |
| unDefName | Agda.TypeChecking.Test.Generators |
| underAbstraction | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| underAbstraction_ | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| Underscore | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| underscore | Agda.Syntax.Concrete.Pretty |
| Undo | Agda.Auto.NarrowingSearch |
| unEl | Agda.Syntax.Internal |
| unequal | Agda.Auto.Typecheck |
| UnequalHiding | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unequals | Agda.Auto.Typecheck |
| UnequalSorts | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTelescopes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTerms | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnequalTypes | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UnexpectedWithPatterns | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unExprView | Agda.Syntax.Concrete.Operators.Parser |
| unflattenTel | Agda.TypeChecking.Telescope |
| unfoldCorecursion | Agda.TypeChecking.CompiledClause.Match |
| unfoldDefinition | Agda.TypeChecking.Reduce, Agda.Interaction.GhciTop |
| unGraph | Agda.Utils.Graph |
| uniConstr | Agda.TypeChecking.Rules.LHS.Unify |
| unification | Agda.Compiler.Epic.Forcing |
| UnificationResult | Agda.TypeChecking.Rules.LHS.Unify |
| Unifies | Agda.TypeChecking.Rules.LHS.Unify |
| Unify | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyException | Agda.TypeChecking.Rules.LHS.Unify |
| unifyexp | Agda.Auto.CaseSplit |
| unifyI | Agda.Compiler.Epic.Forcing |
| unifyIndices | Agda.TypeChecking.Rules.LHS.Unify |
| unifyIndices_ | Agda.TypeChecking.Rules.LHS.Unify |
| UnifyState | Agda.TypeChecking.Rules.LHS.Unify |
| UninstantiatedDotPattern | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| UninstantiatedModule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| union | |
| 1 (Function) | Agda.Utils.Graph |
| 2 (Function) | Agda.Utils.Trie |
| 3 (Function) | Agda.Termination.CallGraph |
| unions | Agda.Utils.Graph |
| unionSignatures | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| unionWithM | Agda.Utils.Map |
| uniSub | Agda.TypeChecking.Rules.LHS.Unify |
| UNIT | Agda.Compiler.Epic.AuxAST |
| univar | Agda.Auto.SearchControl |
| Unknown | Agda.TypeChecking.Positivity |
| unknown | Agda.Termination.CallGraph |
| UnknownName | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| UnknownNamesInFixityDecl | Agda.Syntax.Concrete.Definitions |
| UnknownSort | Agda.Auto.Syntax |
| unlessM | Agda.Utils.Monad |
| unLevelAtom | Agda.TypeChecking.Level |
| unLevelView | Agda.TypeChecking.Level |
| unlistenToMeta | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| unLvl | Agda.TypeChecking.Primitive |
| unnamed | Agda.Syntax.Common |
| unNat | Agda.TypeChecking.Primitive |
| unNoType | Agda.TypeChecking.Test.Generators |
| unqhname | Agda.Compiler.MAlonzo.Misc |
| unqname | Agda.Compiler.Epic.CompileState |
| unqualify | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| UnreachableClauses | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsafeCoerceMod | Agda.Compiler.MAlonzo.Misc |
| unSizedList | Agda.TypeChecking.Test.Generators |
| unSizeView | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| UnsolvedConstraints | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsolvedConstraints | Agda.Interaction.Imports |
| UnsolvedMeta | Agda.Interaction.Highlighting.Precise |
| UnsolvedMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unsolvedMetaVariables | Agda.Interaction.Imports |
| unStr | Agda.TypeChecking.Primitive |
| unTCM | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unUnify | Agda.TypeChecking.Rules.LHS.Unify |
| Unused | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| unVarName | Agda.TypeChecking.Test.Generators |
| unYesType | Agda.TypeChecking.Test.Generators |
| updateMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| updateMetaVar | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| updateMetaVarRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| updatePtr | Agda.Utils.Pointer |
| updateWithConstructorRanges | Agda.TypeChecking.With |
| ureadIORef | Agda.Auto.NarrowingSearch |
| ureadmodifyIORef | Agda.Auto.NarrowingSearch |
| ureduce | Agda.TypeChecking.Rules.LHS.Unify |
| usage | Agda.Interaction.Options |
| usedSeed | Agda.Utils.QuickCheck |
| usedSize | Agda.Utils.QuickCheck |
| useInjectivity | Agda.TypeChecking.Injectivity |
| UseLit | Agda.TypeChecking.Test.Generators |
| useLitChar | Agda.TypeChecking.Test.Generators |
| UseLiterals | Agda.TypeChecking.Test.Generators |
| useLitFloat | Agda.TypeChecking.Test.Generators |
| useLitInt | Agda.TypeChecking.Test.Generators |
| useLitString | Agda.TypeChecking.Test.Generators |
| useNamesFromPattern | Agda.TypeChecking.Rules.LHS |
| Using | Agda.Syntax.Concrete |
| UsingOrHiding | Agda.Syntax.Concrete |
| usingOrHiding | Agda.Syntax.Concrete |
| USt | Agda.TypeChecking.Rules.LHS.Unify |
| uwriteIORef | Agda.Auto.NarrowingSearch |
| validParameters | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
| ValueCmp | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| Var | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Compiler.Epic.AuxAST |
| 3 (Type/Class) | Agda.Compiler.Epic.AuxAST |
| 4 (Data Constructor) | Agda.Syntax.Internal |
| 5 (Data Constructor) | Agda.Syntax.Abstract |
| var | Agda.TypeChecking.Primitive |
| VarArg | Agda.TypeChecking.Positivity |
| varFreq | Agda.TypeChecking.Test.Generators |
| VariableIsIrrelevant | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| variant | Agda.Utils.QuickCheck |
| VarMP | Agda.TypeChecking.Coverage.Match |
| VarName | |
| 1 (Data Constructor) | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| 2 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 3 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| VarP | |
| 1 (Data Constructor) | Agda.Syntax.Internal |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| vcat | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| vector | Agda.Utils.QuickCheck |
| vectorOf | Agda.Utils.QuickCheck |
| verbose | Agda.Utils.QuickCheck |
| verboseBracket | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| verboseCheck | Agda.Utils.QuickCheck |
| verboseCheckResult | Agda.Utils.QuickCheck |
| verboseCheckWith | Agda.Utils.QuickCheck |
| verboseCheckWithResult | Agda.Utils.QuickCheck |
| VerboseKey | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| verboseS | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| Verbosity | Agda.Interaction.Options |
| version | Agda.Version |
| vimFile | Agda.Interaction.Highlighting.Vim |
| VisitedModules | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| visitModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| waitok | Agda.Auto.NarrowingSearch |
| wakeIrrelevantVars | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad |
| wakeupConstraints | Agda.TypeChecking.Constraints |
| Warnings | |
| 1 (Type/Class) | Agda.Interaction.Imports |
| 2 (Data Constructor) | Agda.Interaction.Imports |
| warningsToError | Agda.Interaction.Imports |
| warshall | Agda.Utils.Warshall |
| warshallConstraint | Agda.TypeChecking.UniversePolymorphism |
| warshallG | Agda.Utils.Warshall |
| Weak | Agda.Auto.Syntax |
| weak | Agda.Auto.Syntax |
| weakarglist | Agda.Auto.Syntax |
| weakelr | Agda.Auto.Syntax |
| weaken | Agda.Auto.Convert |
| weakens | Agda.Auto.Convert |
| weaki | Agda.Auto.Syntax |
| Weight | Agda.Utils.Warshall |
| wellFormedIndices | Agda.TypeChecking.Rules.LHS.Split |
| whatInduction | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| whenFail | Agda.Utils.QuickCheck |
| whenFail' | Agda.Utils.QuickCheck |
| whenM | Agda.Utils.Monad |
| WhereClause | Agda.Syntax.Concrete |
| WildMP | Agda.TypeChecking.Coverage.Match |
| WildP | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| withAnonymousModule | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| WithApp | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| withAppBrackets | Agda.Syntax.Fixity |
| WithArgCtx | Agda.Syntax.Fixity |
| withArgsFrom | Agda.Syntax.Common |
| WithClausePatternMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| withConstraint | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad |
| withContextPrecedence | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| withCurrentModule | |
| 1 (Function) | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Syntax.Scope.Monad |
| withCurrentModule' | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| withDisplayForm | Agda.TypeChecking.With |
| withEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad |
| withFresh | Agda.Utils.Fresh |
| WithFunction | Agda.TypeChecking.Rules.Def |
| WithFunctionProblem | Agda.TypeChecking.Rules.Def |
| withFunctionType | Agda.TypeChecking.With |
| WithFunCtx | Agda.Syntax.Fixity |
| withImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad |
| within | Agda.Utils.QuickCheck |
| withInteractionId | Agda.Interaction.BasicOps |
| withInterval | Agda.Syntax.Parser.LexActions |
| withInterval' | Agda.Syntax.Parser.LexActions |
| withInterval_ | Agda.Syntax.Parser.LexActions |
| withLayout | Agda.Syntax.Parser.LexActions, Agda.Syntax.Parser.Layout |
| withLocalVars | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| withMetaId | Agda.Interaction.BasicOps |
| withMetaInfo | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad |
| withRangeOf | Agda.Syntax.Position, Agda.Interaction.GhciTop |
| withRangesOf | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| withRangesOfQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Interaction.GhciTop |
| WithRHS | Agda.Syntax.Abstract |
| withScope | |
| 1 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Syntax.Translation.AbstractToConcrete |
| withScope_ | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| withSignature | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| withTopLevelModule | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| wordsBy | Agda.Utils.List |
| writeFile | Agda.Utils.IO.UTF8 |
| writeInterface | Agda.Interaction.Imports |
| writeModule | Agda.Compiler.MAlonzo.Compiler |
| WrongHidingInApplication | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongHidingInLambda | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongHidingInLHS | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WrongNumberOfConstructorArguments | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| WSM | Agda.Syntax.Scope.Monad, Agda.Interaction.GhciTop |
| xForPrim | Agda.Compiler.MAlonzo.Primitives |
| xhqn | Agda.Compiler.MAlonzo.Misc |
| xqual | Agda.Compiler.MAlonzo.Misc |
| Yes | |
| 1 (Data Constructor) | Agda.TypeChecking.Coverage.Match |
| 2 (Data Constructor) | Agda.TypeChecking.Patterns.Match |
| yesMatchLit | Agda.TypeChecking.Coverage.Match |
| YesReduction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| YesType | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| zero | Agda.Termination.Semiring |
| zeroElement | Agda.Termination.Semiring |
| zeroName | Agda.TypeChecking.Level |
| zeroWidthText | Agda.Utils.Pretty |
| ZigZagMode | Agda.Utils.Pretty |
| zipNameSpace | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| zipScope | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| zipScope_ | Agda.Syntax.Scope.Base, Agda.Interaction.GhciTop |
| zipWith | Agda.Termination.Matrix |
| zipWithM' | Agda.Utils.Monad |
| |-> | Agda.TypeChecking.Rules.LHS.Unify |