| gApply | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| gApply' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| garr | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| gaussJordanFloydWarshallMcNaughtonYamada | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| gaussJordanFloydWarshallMcNaughtonYamadaReference | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| GeneralHelp | Agda.Interaction.Options.Help |
| Generalizable | Agda.Interaction.Highlighting.Precise |
| GeneralizableVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Generalize | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 3 (Data Constructor) | Agda.Syntax.Abstract |
| GeneralizeCyclicDependency | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| Generalized | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| generalized | Agda.Syntax.Abstract |
| generalizedFieldName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GeneralizedValue | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GeneralizedVarsMetadata | Agda.Syntax.Scope.Base |
| GeneralizeName | Agda.Syntax.Scope.Base |
| GeneralizeNotSupportedHere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GeneralizeTel | Agda.Syntax.Abstract |
| generalizeTel | Agda.Syntax.Abstract |
| GeneralizeTelescope | Agda.Syntax.Abstract |
| generalizeTelescope | Agda.TypeChecking.Generalize |
| generalizeTelVars | Agda.Syntax.Abstract |
| generalizeType | Agda.TypeChecking.Generalize |
| generalizeType' | Agda.TypeChecking.Generalize |
| GeneralizeUnsolvedMeta | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| generateAndPrintSyntaxInfo | Agda.Interaction.Highlighting.Generate |
| generateDot | Agda.Interaction.Highlighting.Dot |
| generateHTML | Agda.Interaction.Highlighting.HTML |
| generateHTMLWithPageGen | Agda.Interaction.Highlighting.HTML |
| generateLaTeX | Agda.Interaction.Highlighting.LaTeX |
| generatePage | Agda.Interaction.Highlighting.HTML |
| generateTokenInfo | Agda.Interaction.Highlighting.Generate |
| generateTokenInfoFromSource | Agda.Interaction.Highlighting.Generate |
| generateTokenInfoFromString | Agda.Interaction.Highlighting.Generate |
| generateVimFile | Agda.Interaction.Highlighting.Vim |
| Generator | Agda.Utils.Haskell.Syntax |
| GenericDocError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genericDocError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genericElemIndex | Agda.Utils.List |
| GenericError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genericError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GenericNonFatalError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genericNonFatalError | Agda.TypeChecking.Warnings |
| GenericNonFatalError_ | Agda.Interaction.Options.Warnings |
| GenericSplitError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GenericWarning | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genericWarning | Agda.TypeChecking.Warnings |
| GenericWarning_ | Agda.Interaction.Options.Warnings |
| GenPart | Agda.Syntax.Common |
| genPrimForce | Agda.TypeChecking.Primitive |
| genvalCheckpoint | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genvalTerm | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| genvalType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| getAllArgs | Agda.Auto.Typecheck |
| getAllConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAllInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAllPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAllUnsolved | Agda.Interaction.Imports |
| getAllWarnings | Agda.Interaction.Imports |
| getAllWarnings' | Agda.Interaction.Imports |
| getAllWarningsOfTCErr | Agda.Interaction.Imports |
| getAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAnonymousVariables | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getArgInfo | Agda.Syntax.Common |
| getArgOccurrence | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getAwakeConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBenchmark | |
| 1 (Function) | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark |
| 2 (Function) | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad |
| getblks | Agda.Auto.CaseSplit |
| getBuiltin | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBuiltin' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBuiltinDefName | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBuiltinName | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| getBuiltinName' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBuiltinSize | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getBuiltinThing | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getClausesAsRewriteRules | Agda.TypeChecking.Rewriting.Clause |
| getClauseZipperForIP | Agda.Interaction.MakeCase |
| getClockTime | Agda.Utils.Time |
| getCohesion | Agda.Syntax.Common |
| getCohesionMod | Agda.Syntax.Common |
| getCommandLineOptions | Agda.Interaction.Options.Lenses |
| getCompiled | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getCompiledArgUse | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getConcreteFixity | Agda.Syntax.Scope.Monad |
| getConcretePolarity | Agda.Syntax.Scope.Monad |
| getConForm | Agda.TypeChecking.Datatypes |
| getConHead | Agda.TypeChecking.Datatypes |
| getConHeads | Agda.TypeChecking.Datatypes |
| getConHeads' | Agda.TypeChecking.Datatypes |
| getConInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getConName | Agda.Syntax.Internal |
| getConst | |
| 1 (Function) | Agda.Auto.Syntax |
| 2 (Function) | Agda.Auto.Convert |
| getConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad, Agda.Compiler.Backend |
| getConstInfo' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getConstraints | Agda.Interaction.BasicOps |
| getConstraints' | Agda.Interaction.BasicOps |
| getConstraintsForProblem | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getConstraintsMentioning | Agda.Interaction.BasicOps |
| getConstructorData | Agda.TypeChecking.Datatypes |
| getConstructorInfo | Agda.TypeChecking.Datatypes |
| getConstructors | Agda.TypeChecking.Datatypes |
| getConstructors' | Agda.TypeChecking.Datatypes |
| getConstructors_ | Agda.TypeChecking.Datatypes |
| getContext | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getContextArgs | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getContextNames | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getContextSize | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getContextTelescope | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getContextTerms | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getConType | Agda.TypeChecking.Datatypes |
| getCost | Agda.Auto.NarrowingSearch |
| getCPUTime | Agda.Utils.Time |
| getCurrentModule | Agda.Syntax.Scope.Monad |
| getCurrentModuleFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getCurrentPath | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getCurrentRange | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getCurrentScope | Agda.Syntax.Scope.Monad |
| getDatatype | Agda.Auto.Typecheck |
| getDecodedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getDecodedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getDef | Agda.TypeChecking.Functions |
| getDefArity | Agda.TypeChecking.Positivity |
| getDefaultLibraries | Agda.Interaction.Library |
| getDefFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getDefModule | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GetDefs | Agda.Syntax.Internal.Defs |
| getDefs | Agda.Syntax.Internal.Defs |
| getDefs' | Agda.Syntax.Internal.Defs |
| GetDefsEnv | |
| 1 (Type/Class) | Agda.Syntax.Internal.Defs |
| 2 (Data Constructor) | Agda.Syntax.Internal.Defs |
| GetDefsM | Agda.Syntax.Internal.Defs |
| getDefType | Agda.TypeChecking.Records |
| getdfv | Agda.Auto.Convert |
| getDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getEqs | Agda.Auto.Convert |
| getErasedConArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getForcedArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getFreeVariables | Agda.Syntax.Common |
| getFreeVariablesArgInfo | Agda.Syntax.Common |
| getFullyAppliedConType | Agda.TypeChecking.Datatypes |
| getGeneralizedFieldName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getGeneralizedParameters | Agda.TypeChecking.Rules.Data |
| getGoals | Agda.Interaction.BasicOps |
| getHaskellConstructor | Agda.Compiler.MAlonzo.Pragmas |
| getHaskellPragma | Agda.Compiler.MAlonzo.Pragmas |
| getHiding | Agda.Syntax.Common |
| getHidingArgInfo | Agda.Syntax.Common |
| getImportPath | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getImports | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getIncludeDirs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getIncludePaths | Agda.Interaction.Options.Lenses |
| getinfo | Agda.Auto.SearchControl |
| getInput | Agda.Syntax.Parser.LookAhead |
| getInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInputFile' | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInstalledLibraries | Agda.Interaction.Library |
| getInstanceDefs | Agda.TypeChecking.Telescope |
| getInstantiatedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionIdsAndMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionPoints | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInteractionScope | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getInterface | Agda.Interaction.Imports |
| getInterface' | Agda.Interaction.Imports |
| getInterfaceFileHashes | Agda.Interaction.Imports |
| getInterfaceFileHashes' | Agda.Interaction.Imports |
| getInterface_ | Agda.Interaction.Imports |
| getIntervalFile | Agda.Syntax.Position |
| getIPBoundary | Agda.Interaction.BasicOps |
| getLeftoverPatterns | Agda.TypeChecking.Rules.LHS.Problem |
| getLetBindings | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getLexInput | Agda.Syntax.Parser.Alex |
| getLexState | Agda.Syntax.Parser.Monad |
| getLocalVars | Agda.Syntax.Scope.Monad |
| getMask | Agda.Termination.Monad |
| getMasked | Agda.Termination.Monad |
| GetMatchables | Agda.TypeChecking.Rewriting.NonLinPattern |
| getMatchables | Agda.TypeChecking.Rewriting.NonLinPattern |
| getMaxNat | Agda.Utils.Monoid |
| getMaybeWarnings | Agda.Interaction.Imports |
| getMaybeWarnings' | Agda.Interaction.Imports |
| getMeta | Agda.Auto.Convert |
| getMetaContextArgs | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaEnv | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaInfo | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaListeners | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaModality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaNameSuggestion | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaPriority | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaRange | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaRelevance | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaSig | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaStore | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaType | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaTypeInContext | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaVariables | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMetaVariableSet | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getModality | Agda.Syntax.Common |
| getModalityArgInfo | Agda.Syntax.Common |
| getModuleContents | Agda.Interaction.BasicOps |
| getModuleFreeVars | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getModuleParameterSub | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMutual | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getMutual_ | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getName' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getNamedScope | Agda.Syntax.Scope.Monad |
| getNameOf | Agda.Syntax.Common |
| getNameOfConstrained | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getNArgs | Agda.Auto.Typecheck |
| getNotation | Agda.Syntax.Scope.Monad |
| getNumberOfParameters | Agda.TypeChecking.Datatypes |
| getOccurrences | Agda.TypeChecking.Positivity |
| getOldInteractionScope | Agda.Interaction.InteractionTop |
| getOpen | Agda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getOpenMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getOptSimple | Agda.Interaction.Options |
| getOrigConHead | Agda.TypeChecking.Datatypes |
| getOrigin | Agda.Syntax.Common |
| getOriginalProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getOriginArgInfo | Agda.Syntax.Common |
| getOutputTypeName | Agda.TypeChecking.Telescope |
| getParseFlags | Agda.Syntax.Parser.Monad |
| getParseInterval | Agda.Syntax.Parser.Monad |
| getPartialDefs | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPatternSynImports | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPatternSyns | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPersistentVerbosity | Agda.Interaction.Options.Lenses |
| getPolarity | |
| 1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Function) | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPolarity' | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPragmaOptions | Agda.Interaction.Options.Lenses |
| getPrimitive | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrimitive' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrimitiveName' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrimitiveTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrimitiveTerm' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrimName | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getPrio | Agda.Auto.NarrowingSearch |
| getProjLams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getQuantity | Agda.Syntax.Common |
| getQuantityMod | Agda.Syntax.Common |
| getRange | Agda.Syntax.Position |
| getRecordConstructor | Agda.TypeChecking.Records |
| getRecordContents | Agda.Interaction.BasicOps |
| getRecordDef | Agda.TypeChecking.Records |
| getRecordFieldNames | Agda.TypeChecking.Records |
| getRecordFieldNames_ | Agda.TypeChecking.Records |
| getRecordFieldTypes | Agda.TypeChecking.Records |
| getRecordOfField | Agda.TypeChecking.Records |
| getRecordTypeFields | Agda.TypeChecking.Records |
| getRefl | Agda.TypeChecking.Primitive |
| getReflArgInfo | Agda.TypeChecking.Primitive |
| getRelevance | Agda.Syntax.Common |
| getRelevanceMod | Agda.Syntax.Common |
| getResponseContext | Agda.Interaction.BasicOps |
| getRewriteRulesFor | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getSafeMode | Agda.Interaction.Options.Lenses |
| getsBenchmark | Agda.Utils.Benchmark |
| getScope | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getSection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getSigmaKit | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| getSignature | Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getSimplification | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getSizeConstraints | Agda.TypeChecking.SizedTypes |
| getSizeHypotheses | Agda.TypeChecking.SizedTypes.Solve |
| getSizeMetas | Agda.TypeChecking.SizedTypes |
| getSolvedInteractionPoints | Agda.Interaction.BasicOps |
| getSort | Agda.Syntax.Internal |
| getStatistics | Agda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getsTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getStoredInterface | Agda.Interaction.Imports |
| getTC | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getTCState | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getTerm | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getTerm' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getTimeOut | Agda.Auto.Options |
| getTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getUnambiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| getUniqueCompilerPragma | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getUniqueMetasRanges | Agda.Interaction.Imports |
| getUnsolvedMetas | Agda.Interaction.Imports |
| getUserVariableNames | Agda.TypeChecking.Rules.LHS.Problem |
| getUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getVar | Agda.Auto.Syntax |
| getVarInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getVarsToBind | Agda.Syntax.Scope.Monad |
| getVerbosity | |
| 1 (Function) | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Function) | Agda.Interaction.Options.Lenses |
| getVisitedModule | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| getWarningsAndNonFatalErrors | Agda.Interaction.BasicOps |
| ghcBackend | Agda.Compiler.MAlonzo.Compiler |
| ghcBackend' | Agda.Compiler.MAlonzo.Compiler |
| ghcBackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| ghcCommandLineFlags | Agda.Compiler.MAlonzo.Compiler |
| ghcCompileDef | Agda.Compiler.MAlonzo.Compiler |
| ghcMayEraseType | Agda.Compiler.MAlonzo.Compiler |
| GHCModuleEnv | Agda.Compiler.MAlonzo.Compiler |
| GHCOptions | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| ghcPostCompile | Agda.Compiler.MAlonzo.Compiler |
| ghcPostModule | Agda.Compiler.MAlonzo.Compiler |
| ghcPreCompile | Agda.Compiler.MAlonzo.Compiler |
| ghcPreModule | Agda.Compiler.MAlonzo.Compiler |
| Give | Agda.Interaction.InteractionTop |
| give | Agda.Interaction.BasicOps |
| giveExpr | Agda.Interaction.BasicOps |
| giveMeta | Agda.Interaction.CommandLine |
| GiveRefine | Agda.Interaction.InteractionTop |
| GiveResult | Agda.Interaction.Response |
| giveUp | Agda.TypeChecking.SizedTypes |
| give_gen | Agda.Interaction.InteractionTop |
| Give_NoParen | Agda.Interaction.Response |
| Give_Paren | Agda.Interaction.Response |
| Give_String | Agda.Interaction.Response |
| glam | Agda.TypeChecking.Names |
| glamN | Agda.TypeChecking.Names |
| glb | Agda.TypeChecking.SizedTypes.WarshallSolver |
| glb' | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Global | Agda.Compiler.JS.Syntax |
| global | Agda.Compiler.JS.Compiler |
| global' | Agda.Compiler.JS.Compiler |
| GlobalId | |
| 1 (Type/Class) | Agda.Compiler.JS.Syntax |
| 2 (Data Constructor) | Agda.Compiler.JS.Syntax |
| Globals | Agda.Compiler.JS.Syntax |
| globals | Agda.Compiler.JS.Syntax |
| GM | Agda.Utils.Warshall |
| GoalAndElaboration | Agda.Interaction.Response |
| GoalAndHave | Agda.Interaction.Response |
| GoalDisplayInfo | Agda.Interaction.Response |
| GoalOnly | Agda.Interaction.Response |
| Goals | Agda.Interaction.Response |
| GoalTypeAux | Agda.Interaction.Response |
| Goal_CurrentGoal | Agda.Interaction.Response |
| Goal_GoalType | Agda.Interaction.Response |
| Goal_HelperFunction | Agda.Interaction.Response |
| Goal_InferredType | Agda.Interaction.Response |
| Goal_NormalForm | Agda.Interaction.Response |
| gpi | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| grammar | |
| 1 (Function) | Agda.Utils.Parser.MemoisedCPS |
| 2 (Function) | Agda.Syntax.Concrete.Operators.Parser.Monad |
| Graph | |
| 1 (Type/Class) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Data Constructor) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 3 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
| 4 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| 5 (Type/Class) | Agda.Utils.Warshall |
| 6 (Data Constructor) | Agda.Utils.Warshall |
| 7 (Type/Class) | Agda.TypeChecking.Positivity |
| graph | |
| 1 (Function) | Agda.Utils.Graph.AdjacencyMap.Unidirectional |
| 2 (Function) | Agda.Utils.Warshall |
| graphFromConstraints | Agda.TypeChecking.SizedTypes.WarshallSolver |
| graphFromList | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Graphs | Agda.TypeChecking.SizedTypes.WarshallSolver |
| graphsFromConstraints | Agda.TypeChecking.SizedTypes.WarshallSolver |
| graphToList | Agda.TypeChecking.SizedTypes.WarshallSolver |
| graphToLowerBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| graphToUpperBounds | Agda.TypeChecking.SizedTypes.WarshallSolver |
| Greatest | Agda.TypeChecking.SizedTypes.Syntax |
| groupBy' | Agda.Utils.List |
| groupByEither | Agda.Utils.Either |
| groupOn | Agda.Utils.List |
| groups | Agda.Utils.Bag |
| Guard | Agda.Interaction.Base |
| guardConstraint | Agda.TypeChecking.Constraints |
| Guarded | |
| 1 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 2 (Type/Class) | Agda.Termination.Monad |
| guardednessOption | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| GuardedRhs | |
| 1 (Type/Class) | Agda.Utils.Haskell.Syntax |
| 2 (Data Constructor) | Agda.Utils.Haskell.Syntax |
| GuardedRhss | Agda.Utils.Haskell.Syntax |
| guardM | Agda.Utils.Monad |
| GuardPos | Agda.TypeChecking.Positivity.Occurrence |