| gApply | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| gApply' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| garr | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| Generalized | |
| 1 (Data Constructor) | Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Abstract |
| generalized | Agda.Syntax.Abstract |
| generalizedFieldName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| GeneralizedValue | |
| 1 (Type/Class) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Data Constructor) | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| GeneralizedVarsMetadata | Agda.Syntax.Scope.Base |
| GeneralizeName | Agda.Syntax.Scope.Base |
| GeneralizeNotSupportedHere | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| generateAndPrintSyntaxInfo | Agda.Interaction.Highlighting.Generate |
| 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.Compiler.Backend, Agda.TypeChecking.Monad |
| genericDocError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericElemIndex | Agda.Utils.List |
| GenericError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericFromJSONKey | Agda.Interaction.JSON |
| genericLiftParseJSON | Agda.Interaction.JSON |
| genericLiftToEncoding | Agda.Interaction.JSON |
| genericLiftToJSON | Agda.Interaction.JSON |
| GenericNonFatalError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericNonFatalError | Agda.TypeChecking.Warnings |
| GenericNonFatalError_ | Agda.Interaction.Options.Warnings |
| genericParseJSON | Agda.Interaction.JSON |
| GenericSplitError | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericToEncoding | Agda.Interaction.JSON |
| genericToJSON | Agda.Interaction.JSON |
| genericToJSONKey | Agda.Interaction.JSON |
| GenericUseless | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| GenericUseless_ | Agda.Interaction.Options.Warnings |
| GenericWarning | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genericWarning | Agda.TypeChecking.Warnings |
| GenericWarning_ | Agda.Interaction.Options.Warnings |
| GenPart | Agda.Syntax.Common |
| genPrimForce | Agda.TypeChecking.Primitive |
| genvalCheckpoint | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genvalTerm | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| genvalType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getAbsoluteIncludePaths | Agda.Interaction.Options.Lenses |
| getAgdaLibFiles | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getAgdaLibFiles' | Agda.Interaction.Library |
| getAllArgs | Agda.Auto.Typecheck |
| getAllConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| getAllInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getAllPatternSyns | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getAllUnsolvedWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| getAllWarnings | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| getAllWarningsOfTCErr | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| getAllWarningsPreserving | Agda.TypeChecking.Pretty.Warning, Agda.TypeChecking.Errors |
| getAnnotation | Agda.Syntax.Common |
| getAnonInstanceDefs | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getAnonymousVariables | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| getArgInfo | Agda.Syntax.Common |
| getArgOccurrence | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getAwakeConstraints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getBuiltin' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getBuiltinDefName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| getBuiltinName | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| getBuiltinName' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getBuiltinSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes |
| getBuiltinThing | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getCachedAgdaLibFile | Agda.Interaction.Library.Base |
| getCachedProjectConfig | Agda.Interaction.Library.Base |
| getCallStack | Agda.Utils.CallStack |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getCompiledArgUse | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getConcreteFixity | Agda.Syntax.Scope.Monad |
| getConcretePolarity | Agda.Syntax.Scope.Monad |
| getConForm | Agda.TypeChecking.Datatypes |
| getConHead | Agda.TypeChecking.Datatypes |
| getConInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getConName | Agda.Syntax.Internal |
| getConst | |
| 1 (Function) | Agda.Auto.Syntax |
| 2 (Function) | Agda.Auto.Convert |
| getConstInfo | Agda.Compiler.Backend, Agda.TypeChecking.Reduce.Monad, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getConstInfo' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getConstraints | Agda.Interaction.BasicOps |
| getConstraints' | Agda.Interaction.BasicOps |
| getConstraintsForProblem | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints |
| 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 | |
| 1 (Function) | Agda.Syntax.Parser.Monad |
| 2 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getContextArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getContextNames | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getContextSize | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getContextTelescope | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getContextTerms | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getConType | Agda.TypeChecking.Datatypes |
| getCost | Agda.Auto.NarrowingSearch |
| getCPUTime | Agda.Utils.Time |
| getCurrentModule | Agda.Syntax.Scope.Monad |
| getCurrentModuleFreeVars | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getCurrentPath | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| getCurrentRange | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace |
| getCurrentScope | Agda.Syntax.Scope.Monad |
| getDatatype | Agda.Auto.Typecheck |
| getDecodedModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getDecodedModules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getDef | Agda.TypeChecking.Functions |
| getDefArity | Agda.TypeChecking.Positivity |
| getDefaultLibraries | Agda.Interaction.Library |
| getDefFreeVars | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getDefModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| 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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getEnv | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| getEqs | Agda.Auto.Convert |
| getErasedConArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getForcedArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getFreeVariables | Agda.Syntax.Common |
| getFreeVariablesArgInfo | Agda.Syntax.Common |
| getFullyAppliedConType | Agda.TypeChecking.Datatypes |
| getGeneralizedFieldName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getGeneralizedParameters | Agda.TypeChecking.Rules.Data |
| getGoals | Agda.Interaction.BasicOps |
| getGoals' | Agda.Interaction.BasicOps |
| getHaskellConstructor | Agda.Compiler.MAlonzo.Pragmas |
| getHaskellPragma | Agda.Compiler.MAlonzo.Pragmas |
| getHiding | Agda.Syntax.Common |
| getHidingArgInfo | Agda.Syntax.Common |
| getImportPath | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getImports | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getIncludePaths | Agda.Interaction.Options.Lenses |
| getinfo | Agda.Auto.SearchControl |
| getInput | Agda.Syntax.Parser.LookAhead |
| getInstalledLibraries | Agda.Interaction.Library |
| getInstanceDefs | Agda.TypeChecking.Telescope |
| getInteractionIdsAndMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getInteractionMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getInteractionOutputCallback | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getInteractionPoints | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getInteractionRange | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getInteractionScope | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getInteractor | Agda.Main |
| getIntervalFile | Agda.Syntax.Position |
| getIPBoundary | Agda.Interaction.BasicOps |
| getLanguage | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getLeftoverPatterns | Agda.TypeChecking.Rules.LHS.Problem |
| getLetBindings | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getLexInput | Agda.Syntax.Parser.Alex |
| getLexState | Agda.Syntax.Parser.Monad |
| getLibraryOptions | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getLocalVars | Agda.Syntax.Scope.Monad |
| getLock | Agda.Syntax.Common |
| getMainMode | Agda.Main |
| getMask | Agda.Termination.Monad |
| getMasked | Agda.Termination.Monad |
| GetMatchables | Agda.TypeChecking.Rewriting.NonLinPattern |
| getMatchables | Agda.TypeChecking.Rewriting.NonLinPattern |
| getMaxNat | Agda.Utils.Monoid |
| getMeta | Agda.Auto.Convert |
| getMetaContextArgs | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaEnv | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaInfo | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaListeners | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaModality | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaNameSuggestion | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaPriority | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaRange | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaRelevance | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaScope | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaSig | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getMetaStore | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaType | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaTypeInContext | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getMetaVariables | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getModality | Agda.Syntax.Common |
| getModalityArgInfo | Agda.Syntax.Common |
| getModuleContents | Agda.Interaction.BasicOps |
| getModuleFreeVars | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getModuleParameterSub | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getMutual | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getMutual_ | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getName' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getNamedScope | Agda.Syntax.Scope.Monad |
| getNameOf | Agda.Syntax.Common |
| getNameOfConstrained | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getNArgs | Agda.Auto.Typecheck |
| getNotation | Agda.Syntax.Scope.Monad |
| getNotErasedConstructors | Agda.TypeChecking.Datatypes |
| getNumberOfParameters | Agda.TypeChecking.Datatypes |
| getOccurrences | Agda.TypeChecking.Positivity |
| getOldInteractionScope | Agda.Interaction.InteractionTop |
| getOpen | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Open |
| getOpenMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getOptSimple | Agda.Interaction.Options |
| getOrigConHead | Agda.TypeChecking.Datatypes |
| getOrigin | Agda.Syntax.Common |
| getOriginalConstInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getOriginalProjection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getOriginArgInfo | Agda.Syntax.Common |
| getOutputTypeName | Agda.TypeChecking.Telescope |
| getParseFlags | Agda.Syntax.Parser.Monad |
| getParseInterval | Agda.Syntax.Parser.Monad |
| getPartialDefs | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getPatternSynImports | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getPatternSyns | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getPersistentVerbosity | Agda.Interaction.Options.Lenses |
| getPolarity | |
| 1 (Function) | Agda.TypeChecking.SizedTypes.Syntax |
| 2 (Function) | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getPolarity' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getPragmaOptions | Agda.Interaction.Options.Lenses |
| getPrettyVisitedModules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getPrimitive | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrimitive' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrimitiveLibDir | Agda.Interaction.Library |
| getPrimitiveName' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrimitiveTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrimitiveTerm' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrimName | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getPrio | Agda.Auto.NarrowingSearch |
| getProjLams | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| getReflPattern | Agda.TypeChecking.Rules.Def |
| getRelevance | Agda.Syntax.Common |
| getRelevanceMod | Agda.Syntax.Common |
| getResponseContext | Agda.Interaction.BasicOps |
| getRewriteRulesFor | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getSafeMode | Agda.Interaction.Options.Lenses |
| getsBenchmark | Agda.Utils.Benchmark |
| getScope | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getSection | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getSig | Agda.Syntax.Concrete.Definitions.Monad |
| getSigmaKit | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base |
| getSignature | Agda.TypeChecking.Monad.State, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getSimplification | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Env |
| getSizeConstraints | Agda.TypeChecking.SizedTypes |
| getSizeHypotheses | Agda.TypeChecking.SizedTypes.Solve |
| getSizeMetas | Agda.TypeChecking.SizedTypes |
| getSolvedInteractionPoints | Agda.Interaction.BasicOps |
| getSort | Agda.Syntax.Internal |
| getStatistics | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Statistics |
| getsTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getTC | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getTCState | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getTerm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getTerm' | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin |
| getTimeOut | Agda.Auto.Options |
| getTreeless | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getTrustedExecutables | Agda.Interaction.Library |
| getTypedHead | Agda.TypeChecking.Rewriting.NonLinMatch |
| getUnambiguous | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend |
| getUniqueCompilerPragma | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature |
| getUniqueMetasRanges | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getUniverseCheckFromSig | Agda.Syntax.Concrete.Definitions.Monad |
| getUnsolvedInteractionMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getUnsolvedMetas | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.MetaVars |
| getUserVariableNames | Agda.TypeChecking.Rules.LHS.Problem |
| getUserWarnings | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| getVar | Agda.Auto.Syntax |
| getVarInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Context |
| getVarsToBind | Agda.Syntax.Scope.Monad |
| getVerbosity | |
| 1 (Function) | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 2 (Function) | Agda.Interaction.Options.Lenses |
| getVisitedModule | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getVisitedModules | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Imports |
| getWarningsAndNonFatalErrors | Agda.Interaction.BasicOps |
| GFromJSON | Agda.Interaction.JSON |
| GFromJSONKey | Agda.Interaction.JSON |
| ghcBackend | Agda.Compiler.MAlonzo.Compiler |
| ghcBackend' | Agda.Compiler.MAlonzo.Compiler |
| ghcBackendName | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| ghcCommandLineFlags | Agda.Compiler.MAlonzo.Compiler |
| ghcCompileDef | Agda.Compiler.MAlonzo.Compiler |
| ghcDefDecls | Agda.Compiler.MAlonzo.Compiler |
| ghcDefDefinition | Agda.Compiler.MAlonzo.Compiler |
| ghcDefImports | Agda.Compiler.MAlonzo.Compiler |
| GHCDefinition | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| ghcDefMainDef | Agda.Compiler.MAlonzo.Compiler |
| ghcDefUsesFloat | Agda.Compiler.MAlonzo.Compiler |
| GHCEnv | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Misc |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc |
| ghcEnvBool | Agda.Compiler.MAlonzo.Misc |
| ghcEnvConId | Agda.Compiler.MAlonzo.Misc |
| ghcEnvCons | Agda.Compiler.MAlonzo.Misc |
| ghcEnvFalse | Agda.Compiler.MAlonzo.Misc |
| ghcEnvFlat | Agda.Compiler.MAlonzo.Misc |
| ghcEnvId | Agda.Compiler.MAlonzo.Misc |
| ghcEnvInf | Agda.Compiler.MAlonzo.Misc |
| ghcEnvInteger | Agda.Compiler.MAlonzo.Misc |
| ghcEnvInterval | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIOne | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIsOne | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIsOne1 | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIsOne2 | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIsOneEmpty | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIsTCBuiltin | Agda.Compiler.MAlonzo.Misc |
| ghcEnvItIsOne | Agda.Compiler.MAlonzo.Misc |
| ghcEnvIZero | Agda.Compiler.MAlonzo.Misc |
| ghcEnvJust | Agda.Compiler.MAlonzo.Misc |
| ghcEnvList | Agda.Compiler.MAlonzo.Misc |
| ghcEnvMaybe | Agda.Compiler.MAlonzo.Misc |
| ghcEnvNat | Agda.Compiler.MAlonzo.Misc |
| ghcEnvNil | Agda.Compiler.MAlonzo.Misc |
| ghcEnvNothing | Agda.Compiler.MAlonzo.Misc |
| ghcEnvOpts | Agda.Compiler.MAlonzo.Misc |
| ghcEnvPathP | Agda.Compiler.MAlonzo.Misc |
| ghcEnvSharp | Agda.Compiler.MAlonzo.Misc |
| ghcEnvSub | Agda.Compiler.MAlonzo.Misc |
| ghcEnvSubIn | Agda.Compiler.MAlonzo.Misc |
| ghcEnvTrue | Agda.Compiler.MAlonzo.Misc |
| ghcEnvWord64 | Agda.Compiler.MAlonzo.Misc |
| GHCFlags | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| ghcMayEraseType | Agda.Compiler.MAlonzo.Compiler |
| ghcModEnv | Agda.Compiler.MAlonzo.Misc |
| ghcModHsModuleEnv | Agda.Compiler.MAlonzo.Misc |
| ghcModMainFuncs | Agda.Compiler.MAlonzo.Compiler |
| ghcModModuleEnv | Agda.Compiler.MAlonzo.Compiler |
| GHCModule | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Compiler |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Compiler |
| GHCModuleEnv | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Misc |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc |
| GHCOptions | |
| 1 (Type/Class) | Agda.Compiler.MAlonzo.Misc |
| 2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc |
| 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 |
| 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 |
| GlobalCandidate | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| GlobalConfluenceCheck | Agda.Interaction.Options |
| 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, Agda.TypeChecking.Primitive.Base |
| 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 |
| Group | Agda.Compiler.JS.Pretty |
| group | |
| 1 (Function) | Agda.Utils.List1 |
| 2 (Function) | Agda.Compiler.JS.Pretty |
| group1 | Agda.Utils.List1 |
| groupAllWith | Agda.Utils.List1 |
| groupAllWith1 | Agda.Utils.List1 |
| groupBy | Agda.Utils.List1 |
| groupBy' | |
| 1 (Function) | Agda.Utils.List |
| 2 (Function) | Agda.Utils.List1 |
| groupBy1 | Agda.Utils.List1 |
| groupByEither | Agda.Utils.Either |
| groupOn | Agda.Utils.List |
| groups | Agda.Utils.Bag |
| groupWith | Agda.Utils.List1 |
| groupWith1 | Agda.Utils.List1 |
| GToEncoding | Agda.Interaction.JSON |
| GToJSON | Agda.Interaction.JSON |
| GToJSON' | Agda.Interaction.JSON |
| GToJSONKey | Agda.Interaction.JSON |
| guardConstraint | Agda.TypeChecking.Constraints |
| Guarded | Agda.Termination.Monad |
| guardednessOption | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad |
| 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 |
| guardWithError | Agda.Utils.Monad |