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

Index - G

gApplyAgda.TypeChecking.Primitive
garrAgda.TypeChecking.Primitive
gatherAgda.Utils.ReadP
gaussJordanFloydWarshallMcNaughtonYamadaAgda.Utils.Graph.AdjacencyMap.Unidirectional
gaussJordanFloydWarshallMcNaughtonYamadaReferenceAgda.Utils.Graph.AdjacencyMap.Unidirectional
GaveUpAgda.Utils.QuickCheck
GenAgda.Utils.QuickCheck
genArgsAgda.TypeChecking.Test.Generators
GenCAgda.TypeChecking.Test.Generators
genCAgda.TypeChecking.Test.Generators
genConfAgda.TypeChecking.Test.Generators
genElimsAgda.TypeChecking.Test.Generators
generateAgda.Utils.QuickCheck
generateAndPrintSyntaxInfoAgda.Interaction.Highlighting.Generate
generateDotAgda.Interaction.Highlighting.Dot
generateHTMLAgda.Interaction.Highlighting.HTML
generateHTMLWithPageGenAgda.Interaction.Highlighting.HTML
generateLaTeXAgda.Interaction.Highlighting.LaTeX
generatePageAgda.Interaction.Highlighting.HTML
generateTokenInfoAgda.Interaction.Highlighting.Generate
generateTokenInfoFromStringAgda.Interaction.Highlighting.Generate
generateVimFileAgda.Interaction.Highlighting.Vim
genericCoarbitraryAgda.Utils.QuickCheck
GenericDocErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
genericElemIndexAgda.Utils.List
GenericErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
genericErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
genericShrinkAgda.Utils.QuickCheck
GenericSplitErrorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
GenericUnifyExceptionAgda.TypeChecking.Rules.LHS.Unify
genGraphAgda.Utils.Warshall
genGraph_Agda.Utils.Warshall
GenPartAgda.Syntax.Notation
genPathAgda.Utils.Warshall
getAgda.Utils.ReadP
getAllArgsAgda.Auto.Typecheck
getAllConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getAllInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getAnonInstanceDefsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getAnonymousVariablesAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getArgOccurrenceAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getBenchmark 
1 (Function)Agda.Utils.Benchmark, Agda.TypeChecking.Monad.Benchmark
2 (Function)Agda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getBlindAgda.Utils.QuickCheck
getblksAgda.Auto.CaseSplit
GetBodyAgda.TypeChecking.Substitute
getBodyAgda.TypeChecking.Substitute
getBodyUnraisedAgda.TypeChecking.Substitute
getBrVarsAgda.Compiler.Epic.AuxAST
getBuiltinAgda.TypeChecking.Monad.Builtin
getBuiltin'Agda.TypeChecking.Monad.Builtin
getBuiltinDefNameAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
getBuiltinsAgda.Compiler.Epic.Primitive
getBuiltinSizeAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad
getBuiltinThingAgda.TypeChecking.Monad.Builtin
getClockTimeAgda.Utils.Time
getCommandLineOptionsAgda.Interaction.Options.Lenses
getConArityAgda.Compiler.Epic.CompileState
getConDataAgda.Compiler.Epic.CompileState
getConFormAgda.TypeChecking.Datatypes
getConHeadAgda.TypeChecking.Datatypes
getConInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getConNameAgda.Syntax.Internal
getConstAgda.Auto.Convert
getConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.TypeChecking.Reduce.Monad
getConstraintsAgda.Interaction.BasicOps
getConstraintsForProblemAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getConstrTagAgda.Compiler.Epic.CompileState
getConstrTag'Agda.Compiler.Epic.CompileState
getConstructorArityAgda.TypeChecking.Datatypes
getConstructorDataAgda.TypeChecking.Datatypes
getConTermAgda.TypeChecking.Datatypes
getContextAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextArgsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextIdAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextPrecedenceAgda.Syntax.Scope.Monad
getContextSizeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTelescopeAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getContextTermsAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getConTypeAgda.TypeChecking.Datatypes
getCPUTimeAgda.Utils.Time
getCurrentModuleAgda.Syntax.Scope.Monad
getCurrentRangeAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad
getCurrentScopeAgda.Syntax.Scope.Monad
getDataConAgda.Compiler.Epic.CompileState
getDatatypeAgda.Auto.Typecheck
getDecodedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDecodedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getDefArityAgda.TypeChecking.Positivity
getDefFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
GetDefInfoAgda.Syntax.Abstract
getDefInfoAgda.Syntax.Abstract
GetDefsAgda.Syntax.Internal.Defs
getDefsAgda.Syntax.Internal.Defs
getDefs'Agda.Syntax.Internal.Defs
GetDefsEnv 
1 (Type/Class)Agda.Syntax.Internal.Defs
2 (Data Constructor)Agda.Syntax.Internal.Defs
GetDefsMAgda.Syntax.Internal.Defs
getDefTypeAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getDelayedAgda.Compiler.Epic.CompileState
getdfvAgda.Auto.Convert
getEnvAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getEqsAgda.Auto.Convert
getFixedAgda.Utils.QuickCheck
getForcedArgsAgda.Compiler.Epic.CompileState
getHaskellImportsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getHidingAgda.Syntax.Common
getHsTypeAgda.Compiler.HaskellTypes
getHsVarAgda.Compiler.HaskellTypes
getImportedSignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getImportPathAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getImportsAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getIncludeDirs 
1 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
2 (Function)Agda.Interaction.Options.Lenses
getinfoAgda.Auto.SearchControl
getInputAgda.Syntax.Parser.LookAhead
getInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getInputFile'Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getInstanceDefsAgda.TypeChecking.Telescope
getInstantiatedMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionIdsAndMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionOutputCallbackAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getInteractionPointsAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInteractionScopeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getInterfaceAgda.Interaction.Imports
getInterface'Agda.Interaction.Imports
getInterfaceFileHashesAgda.Interaction.Imports
getInterface_Agda.Interaction.Imports
getLargeAgda.Utils.QuickCheck
getLexInputAgda.Syntax.Parser.Alex
getLexStateAgda.Syntax.Parser.Monad
getLocalVarsAgda.Syntax.Scope.Monad
getMainAgda.Compiler.Epic.CompileState
getMaskAgda.Termination.Monad
getMaskedAgda.Termination.Monad
getMetaAgda.Auto.Convert
getMetaColorsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaEnvAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaInfoAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaListenersAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaNameSuggestionAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaPriorityAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRangeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaRelevanceAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaScopeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaSigAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
getMetaStoreAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaTypeAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getMetaTypeInContextAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getModuleFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getMutualBlocksAgda.TypeChecking.Monad.Mutual, Agda.TypeChecking.Monad
getNamedScopeAgda.Syntax.Scope.Monad
getNArgsAgda.Auto.Typecheck
getNatishAgda.Compiler.Epic.NatDetection
getNonEmptyAgda.Utils.QuickCheck
getNonNegativeAgda.Utils.QuickCheck
getNonZeroAgda.Utils.QuickCheck
getNotationAgda.Syntax.Scope.Monad
getNumberOfParametersAgda.TypeChecking.Datatypes
getOccurrencesAgda.TypeChecking.Positivity
getOldInteractionScopeAgda.Interaction.InteractionTop
getOpenAgda.TypeChecking.Monad.Open, Agda.TypeChecking.Monad
getOpenMetasAgda.TypeChecking.Monad.MetaVars, Agda.TypeChecking.Monad
getOptSimpleAgda.Interaction.Options
getOrderedAgda.Utils.QuickCheck
getOrigConHeadAgda.TypeChecking.Datatypes
getOrigConTermAgda.TypeChecking.Datatypes
getOriginalProjectionAgda.TypeChecking.Records
getOutputTypeNameAgda.TypeChecking.Telescope
getParseFlagsAgda.Syntax.Parser.Monad
getParseIntervalAgda.Syntax.Parser.Monad
getPatternSynImportsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getPatternSynsAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getPersistentVerbosityAgda.Interaction.Options.Lenses
getPolarity 
1 (Function)Agda.TypeChecking.SizedTypes.Syntax
2 (Function)Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPolarity'Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getPositiveAgda.Utils.QuickCheck
getPragmaOptionsAgda.Interaction.Options.Lenses
getPrimitiveAgda.TypeChecking.Monad.Builtin
getPrimitive'Agda.TypeChecking.Monad.Builtin
getRangeAgda.Syntax.Position
getRecordConstructorAgda.TypeChecking.Records
getRecordConstructorTypeAgda.TypeChecking.Records
getRecordDefAgda.TypeChecking.Records
getRecordFieldNamesAgda.TypeChecking.Records
getRecordFieldTypesAgda.TypeChecking.Records
getRecordOfFieldAgda.TypeChecking.Records
getRecordTypeFieldsAgda.TypeChecking.Records
getRelevanceAgda.Syntax.Common
getRewriteRulesForAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getSafeModeAgda.Interaction.Options.Lenses
getsBenchmarkAgda.Utils.Benchmark
getScopeAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getSecFreeVarsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getSectionAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getsEIAgda.Compiler.Epic.CompileState
getShrink2Agda.Utils.QuickCheck
getSignatureAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad
getSimplificationAgda.TypeChecking.Monad.Env, Agda.TypeChecking.Monad
getSizeConstraintsAgda.TypeChecking.SizedTypes
getSizeHypothesesAgda.TypeChecking.SizedTypes.Solve
getSizeMetasAgda.TypeChecking.SizedTypes
getSmallAgda.Utils.QuickCheck
getSolvedInteractionPointsAgda.Interaction.BasicOps
getSortAgda.Syntax.Internal
getStatisticsAgda.TypeChecking.Monad.Statistics, Agda.TypeChecking.Monad
getSubAgda.TypeChecking.Rules.LHS.Unify
getTypeAgda.Compiler.Epic.CompileState
getVarInfoAgda.TypeChecking.Monad.Context, Agda.TypeChecking.Monad
getVerbosity 
1 (Function)Agda.Interaction.Options.Lenses
2 (Function)Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad
getVisitedModuleAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
getVisitedModulesAgda.TypeChecking.Monad.Imports, Agda.TypeChecking.Monad
GiveAgda.Interaction.InteractionTop
giveAgda.Interaction.BasicOps
giveExprAgda.Interaction.BasicOps
giveMetaAgda.Interaction.CommandLine
GiveRefineAgda.Interaction.InteractionTop
GiveResultAgda.Interaction.Response
give_genAgda.Interaction.InteractionTop
Give_NoParenAgda.Interaction.Response
Give_ParenAgda.Interaction.Response
Give_StringAgda.Interaction.Response
glbAgda.TypeChecking.SizedTypes.WarshallSolver
glb'Agda.TypeChecking.SizedTypes.WarshallSolver
GlobalAgda.Compiler.JS.Syntax
globalAgda.Compiler.JS.Compiler
global'Agda.Compiler.JS.Compiler
GlobalId 
1 (Type/Class)Agda.Compiler.JS.Syntax
2 (Data Constructor)Agda.Compiler.JS.Syntax
globalidAgda.Compiler.JS.Parser
GlobalsAgda.Compiler.JS.Syntax
globalsAgda.Compiler.JS.Syntax
GMAgda.Utils.Warshall
goAgda.TypeChecking.Free.Lazy
goIrrelevantAgda.TypeChecking.MetaVars.Occurs
goRelAgda.TypeChecking.Free.Lazy
gpiAgda.TypeChecking.Primitive
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
graphFromConstraintsAgda.TypeChecking.SizedTypes.WarshallSolver
graphFromListAgda.TypeChecking.SizedTypes.WarshallSolver
GraphsAgda.TypeChecking.SizedTypes.WarshallSolver
graphsFromConstraintsAgda.TypeChecking.SizedTypes.WarshallSolver
graphToListAgda.TypeChecking.SizedTypes.WarshallSolver
graphToLowerBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
graphToUpperBoundsAgda.TypeChecking.SizedTypes.WarshallSolver
GreatestAgda.TypeChecking.SizedTypes.Syntax
groupBy'Agda.Utils.List
groupOnAgda.Utils.List
groupsAgda.Utils.Bag
growingElementsAgda.Utils.QuickCheck
GuardAgda.Interaction.BasicOps
guardConstraintAgda.TypeChecking.Constraints
Guarded 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Termination.Monad
GuardPosAgda.TypeChecking.Positivity.Occurrence