Agda-2.8.0: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- #
- $
- %
- &
- +
- .
- /
- <
- =
- >
- ?
- @
- \
- ^
- |
- -
- _
- All

Index - G

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
GeneralizeCyclicDependency_ | Agda.Interaction.Options.Errors
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
GeneralizedVarInLetOpenedModule_ | Agda.Interaction.Options.Errors
GeneralizedVarsMetadata | Agda.Syntax.Scope.Base
GeneralizeName | Agda.Syntax.Scope.Base
GeneralizeNotSupportedHere | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
GeneralizeNotSupportedHere_ | Agda.Interaction.Options.Errors
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
generateAndPrintSyntaxInfo | Agda.Interaction.Highlighting.Generate
GeneratedClause | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
generateLaTeXIO | Agda.Interaction.Highlighting.LaTeX.Base
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
GenericDocError_ | Agda.Interaction.Options.Errors
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
GenericError_ | Agda.Interaction.Options.Errors
GenericException | 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
GenericSplitError_ | Agda.Interaction.Options.Errors
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.Setup
getAgdaLibFile | Agda.Interaction.Library
getAgdaLibFiles | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
getBackendName | Agda.Interaction.InteractionTop
getBenchmark | Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
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
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
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
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
getContextVars | Agda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad, Agda.Compiler.Backend
getContextVars' | 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
getDataDir | Agda.Setup
getDataFileName | Agda.Setup
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
GetFileId | Agda.Utils.FileId
getFileId | Agda.Utils.FileId
getFilteredRewriteRulesFor | 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
GetIdFile | Agda.Utils.FileId
getIdFile | Agda.Utils.FileId
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
getInterface | Agda.Interaction.Imports
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
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
getModalPolarity | 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
getNonMainInterface | Agda.Interaction.Imports
getNonMainModuleInfo | Agda.Interaction.Imports
getNotation | Agda.Syntax.Scope.Monad
getNotErasedConstructors | Agda.TypeChecking.Datatypes
getNumberOfParameters | Agda.TypeChecking.Datatypes
getOccurrences | Agda.TypeChecking.Positivity
getOccurrencesFromType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
getOpt | Agda.Utils.GetOpt
getOpt' | Agda.Utils.GetOpt
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
getPolarityMod | Agda.Syntax.Common
getPragmaOptions | Agda.Interaction.Options
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
getRangeWithoutFile | Agda.Syntax.Position
getRecordConstructor |
1 (Function) | Agda.Syntax.Scope.Monad
2 (Function) | 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
GHCBackendError |
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
ghcBackendError | Agda.Compiler.MAlonzo.Misc
ghcBackendErrorName | Agda.TypeChecking.Errors.Names
ghcBackendErrorNameString | Agda.Interaction.Options.Errors
GHCBackendError_ |
1 (Type/Class) | Agda.Interaction.Options.Errors
2 (Data Constructor) | Agda.Interaction.Options.Errors
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
ghcEnvCons | Agda.Compiler.MAlonzo.Misc
ghcEnvFalse | Agda.Compiler.MAlonzo.Misc
ghcEnvFlat | 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_ | Agda.Interaction.BasicOps
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
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.TypeChecking.Positivity
5 (Type/Class) | Agda.TypeChecking.SizedTypes.WarshallSolver
graph | Agda.Utils.Graph.AdjacencyMap.Unidirectional
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
guard | Agda.Utils.Monad
guardConstraint | Agda.TypeChecking.Constraints
Guarded | Agda.Termination.Monad
GuardednessHelps | Agda.Termination.Termination
GuardednessHelpsNot | Agda.Termination.Termination
GuardednessHelpsYes | Agda.Termination.Termination
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