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 |
genArray | Agda.Utils.IArray |
GeneralHelp | Agda.Interaction.Options.Help |
Generalizable | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise |
GeneralizableVar | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
Generalization | Agda.Syntax.Common |
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 |
GeneralizedVarInLetOpenedModule | 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 |
GeneralizeS | Agda.Syntax.Abstract |
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 |
GeneratedClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
genericFromJSONKey | Agda.Interaction.JSON |
genericLiftParseJSON | Agda.Interaction.JSON |
genericLiftToEncoding | Agda.Interaction.JSON |
genericLiftToJSON | Agda.Interaction.JSON |
genericParseJSON | Agda.Interaction.JSON |
GenericSplitError | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
genericToEncoding | Agda.Interaction.JSON |
genericToJSON | Agda.Interaction.JSON |
genericToJSONKey | Agda.Interaction.JSON |
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 |
getAgdaAppDir | Agda.Interaction.Library |
getAgdaLibFiles | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getAgdaLibFiles' | Agda.Interaction.Library |
getAgdaLibFilesWithoutTopLevelModuleName | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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.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 |
getBlocker | Agda.Syntax.Internal.Blockers, Agda.Syntax.Internal |
getBoundary | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
getBuiltinId | Agda.Syntax.Builtin, Agda.TypeChecking.Monad.Builtin, 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 |
getBuiltinRewriteRelations | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getBuiltinRewriteRelations' | 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 |
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.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 |
getConInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getConName | Agda.Syntax.Internal |
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 |
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.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 |
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 |
getDatatypeArgs | Agda.TypeChecking.Datatypes |
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 |
getDefinedNames | Agda.Syntax.Scope.Flat |
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 |
getDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getEnv | Agda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getEquality | Agda.TypeChecking.Rules.LHS.Unify.Types |
getEqualityUnraised | Agda.TypeChecking.Rules.LHS.Unify.Types |
getErasedConArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getForcedArgs | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getForeignCodeStack | Agda.TypeChecking.Monad.Base, 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 |
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 |
getIncludeDirs | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getIncludePaths | Agda.Interaction.Options.Lenses |
getInput | Agda.Syntax.Parser.LookAhead |
getInstalledLibraries | Agda.Interaction.Library |
getInstanceCandidates | Agda.TypeChecking.InstanceArguments |
getInstanceDefs | Agda.TypeChecking.InstanceArguments |
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 |
getInteractor | Agda.Main |
getIntervalFile | Agda.Syntax.Position |
getIPBoundary | Agda.Interaction.BasicOps |
getLanguage | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
getLibraryOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |
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 |
getMetaScope | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getMetaSig | Agda.TypeChecking.Monad.Base, 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 |
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 |
getNotation | Agda.Syntax.Scope.Monad |
getNotErasedConstructors | Agda.TypeChecking.Datatypes |
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 |
getOriginalConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getOriginalProjection | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getOriginArgInfo | Agda.Syntax.Common |
getOutputTypeName | Agda.TypeChecking.InstanceArguments |
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 |
getPrettyVisitedModules | Agda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getPrimitive | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getPrimitive' | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getPrimitiveLibDir | Agda.Interaction.Library |
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 |
getProfileOptions | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getProjLams | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getQNameFromTerm | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
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 |
getRecordOfField | Agda.TypeChecking.Records |
getRecordTypeFields | Agda.TypeChecking.Records |
getReducedEquality | Agda.TypeChecking.Rules.LHS.Unify.Types |
getReducedEqualityUnraised | Agda.TypeChecking.Rules.LHS.Unify.Types |
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.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 |
getSig | Agda.Syntax.Concrete.Definitions.Monad |
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 |
getTacticAttr | Agda.Syntax.Parser.Helpers |
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 |
getTreeless | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getUniqueMetasRanges | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getUniverseCheckFromSig | Agda.Syntax.Concrete.Definitions.Monad |
getUnsolvedInteractionMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getUnsolvedMetas | Agda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getUserVariableNames | Agda.TypeChecking.Rules.LHS.Problem |
getUserWarnings | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getVarInfo | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
getVarsToBind | Agda.Syntax.Scope.Monad |
getVarType | Agda.TypeChecking.Rules.LHS.Unify.Types |
getVarTypeUnraised | Agda.TypeChecking.Rules.LHS.Unify.Types |
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 |
GFromJSON | Agda.Interaction.JSON |
GFromJSONKey | Agda.Interaction.JSON |
ghcBackend | Agda.Compiler.MAlonzo.Compiler |
ghcBackendName | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
ghcEnvListArity | Agda.Compiler.MAlonzo.Misc |
ghcEnvMaybe | Agda.Compiler.MAlonzo.Misc |
ghcEnvMaybeArity | 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 |
ghcInvocationStrings | Agda.Compiler.MAlonzo.Compiler |
ghcModEnv | Agda.Compiler.MAlonzo.Misc |
ghcModHsModuleEnv | Agda.Compiler.MAlonzo.Misc |
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 |
Give | Agda.Interaction.InteractionTop |
give | Agda.Interaction.BasicOps |
giveExpr | Agda.Interaction.BasicOps |
GiveRefine | Agda.Interaction.InteractionTop |
GiveResult | Agda.Interaction.Response.Base, Agda.Interaction.Response |
giveUp | Agda.TypeChecking.SizedTypes |
give_gen | Agda.Interaction.InteractionTop |
Give_NoParen | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Give_Paren | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Give_String | Agda.Interaction.Response.Base, 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.TypeChecking.Monad, Agda.Compiler.Backend |
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.Base, Agda.Interaction.Response |
GoalAndHave | Agda.Interaction.Response.Base, Agda.Interaction.Response |
GoalDisplayInfo | Agda.Interaction.Response |
GoalDisplayInfo_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response |
GoalOnly | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goals | Agda.Interaction.Response |
Goals_boot | Agda.Interaction.Response.Base, Agda.Interaction.Response |
GoalTypeAux | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goal_CurrentGoal | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goal_GoalType | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goal_HelperFunction | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goal_InferredType | Agda.Interaction.Response.Base, Agda.Interaction.Response |
Goal_NormalForm | Agda.Interaction.Response.Base, Agda.Interaction.Response |
goTickIcode | Agda.TypeChecking.Serialise.Base |
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 (Data Constructor) | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
4 (Type/Class) | Agda.Utils.Warshall |
5 (Data Constructor) | Agda.Utils.Warshall |
6 (Type/Class) | Agda.TypeChecking.Positivity |
7 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver |
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' | Agda.Utils.List1 |
groupBy1 | Agda.Utils.List1 |
groupByEither | Agda.Utils.Either |
groupByFst | Agda.Utils.List1 |
groupByFst1 | Agda.Utils.List1 |
groupOn | Agda.Utils.List1 |
groupOn1 | Agda.Utils.List1 |
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.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 |
guardPointerEquality | Agda.TypeChecking.Conversion |
GuardPos | Agda.TypeChecking.Positivity.Occurrence |
guardWithError | Agda.Utils.Monad |