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

Index - G

gApplyAgda.TypeChecking.Primitive
garrAgda.TypeChecking.Primitive
gatherAgda.Utils.ReadP
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
getArgOccurrencesAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad
getAwakeConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad
getBenchmarkAgda.TypeChecking.Monad.State, Agda.TypeChecking.Monad.Benchmark, 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
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
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
getSafeModeAgda.Interaction.Options.Lenses
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
goIrrelevantAgda.TypeChecking.MetaVars.Occurs
gpiAgda.TypeChecking.Primitive
Graph 
1 (Type/Class)Agda.Utils.Graph.AdjacencyMap
2 (Data Constructor)Agda.Utils.Graph.AdjacencyMap
3 (Type/Class)Agda.Utils.Graph.AdjacencyMap.Unidirectional
4 (Data Constructor)Agda.Utils.Graph.AdjacencyMap.Unidirectional
5 (Type/Class)Agda.TypeChecking.SizedTypes.WarshallSolver
6 (Data Constructor)Agda.TypeChecking.Monad.Base.Benchmark, Agda.TypeChecking.Monad.Benchmark
7 (Type/Class)Agda.Utils.Warshall
8 (Data Constructor)Agda.Utils.Warshall
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
guardAgda.Utils.Monad
guardConstraintAgda.TypeChecking.Constraints
Guarded 
1 (Data Constructor)Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad
2 (Type/Class)Agda.Termination.Monad
GuardPosAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad