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

Index - H

HAgda.Auto.Options
handleCommandAgda.Interaction.InteractionTop
handleCommand_Agda.Interaction.InteractionTop
handleImpossibleAgda.Utils.Impossible
handleImpossibleJustAgda.Utils.Impossible
HandleSolAgda.Auto.NarrowingSearch
hang 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
hasBadRigidAgda.TypeChecking.MetaVars.Occurs
HasBiggerSortAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasBiggerSortAgda.TypeChecking.Sort
HasBuiltinsAgda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasCallStackAgda.Utils.CallStack
hasCatchAllAgda.TypeChecking.CompiledClause
HasConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasCopatternsAgda.Syntax.Concrete.Pattern
hasDefPAgda.Syntax.Internal.Pattern
hasElemAgda.Utils.List
hasElimsAgda.Syntax.Internal
HasEllipsisAgda.Syntax.Concrete.Pattern
hasEllipsisAgda.Syntax.Concrete.Pattern
hasEllipsis'Agda.Syntax.Concrete.Pattern
HasEtaAgda.Syntax.Common
HasEta'Agda.Syntax.Common
HasEta0Agda.Syntax.Common
hasExactVerbosityAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasFreeAgda.Compiler.Treeless.Subst
HasFreshAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HashAgda.Utils.Hash
hashByteStringAgda.Utils.Hash
hashRawTopLevelModuleNameAgda.Syntax.TopLevelModuleName
hashStringAgda.Utils.Hash
HashTableAgda.Utils.HashTable
hashTextAgda.Utils.Hash
hashTextFileAgda.Utils.Hash
HaskellCodeAgda.Compiler.MAlonzo.Pragmas
HaskellPragmaAgda.Compiler.MAlonzo.Pragmas
haskellStringLiteralAgda.Utils.String
HaskellTypeAgda.Compiler.MAlonzo.Pragmas
haskellTypeAgda.Compiler.MAlonzo.HaskellTypes
hasLeftAdjointAgda.Utils.POMonoid
hasLineNumberAgda.Interaction.Library.Base
hasLoopingDisplayFormAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasNoFreeVariablesAgda.Syntax.Common
HasOptionsAgda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasProfileOptionAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasProjectionPatternsAgda.TypeChecking.CompiledClause
HasPTSRuleAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasPTSRuleAgda.TypeChecking.Sort
hasQuantity0Agda.Syntax.Common
hasQuantity1Agda.Syntax.Common
hasQuantityωAgda.Syntax.Common
HasRangeAgda.Syntax.Position
HasTagAgda.Utils.BiMap
hasTwinMetaAgda.TypeChecking.MetaVars
HasTypeAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasUniversePolymorphismAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasVerbosityAgda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasWithPatternsAgda.Syntax.Concrete.Pattern
HasZeroAgda.Termination.Semiring
haveLevelsAgda.TypeChecking.Level
haveSizedTypesAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
haveSizeLtAgda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hcat 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
hcompAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
HCompOpAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
HeadAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
head 
1 (Function)Agda.Utils.List1
2 (Function)Agda.Utils.List2
headAmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
headCallSiteAgda.Utils.CallStack
HeadComputeAgda.Interaction.Base
HeadNormalAgda.Interaction.Base
headPrecedenceAgda.Syntax.Fixity
headStopAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
headSymbolAgda.TypeChecking.Injectivity
headSymbol'Agda.TypeChecking.Injectivity
headWithDefaultAgda.Utils.List
HelpAgda.Interaction.Options.Help
HelpForAgda.Interaction.Options.Help
helpForLocaleErrorAgda.Main
helpTopicUsageAgda.Interaction.Options.Help
hequalMetavarAgda.Auto.NarrowingSearch
hfillAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
HI 
1 (Type/Class)Agda.Auto.CaseSplit
2 (Data Constructor)Agda.Auto.CaseSplit
HiddenAgda.Syntax.Common
hiddenAgda.Syntax.Common
HiddenArgAgda.Syntax.Concrete
HiddenArgVAgda.Syntax.Concrete.Operators.Parser
HiddenGeneralizeAgda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
HiddenGeneralize_Agda.Interaction.Options.Warnings
HiddenPAgda.Syntax.Concrete
hideAgda.Syntax.Common
hideAndRelParamsAgda.TypeChecking.Irrelevance
hideOrKeepInstanceAgda.Syntax.Common
HidingAgda.Syntax.Common
hidingAgda.Syntax.Common
HidingDirectiveAgda.Syntax.Concrete
HidingDirective'Agda.Syntax.Common
HidingMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HidingOnlyAgda.Syntax.Scope.Base
highlightAsTypeCheckedAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
highlightExprAgda.Interaction.InteractionTop
HighlightingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
HighlightingInfoAgda.Interaction.Highlighting.Precise
HighlightingInfoBuilderAgda.Interaction.Highlighting.Precise
highlightingInfoBuilderInvariantAgda.Interaction.Highlighting.Precise
highlightingInfoInvariantAgda.Interaction.Highlighting.Precise
HighlightingLevelAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HighlightingMethodAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HighlightModuleContentsAgda.TypeChecking.Rules.Decl
highlightWarningAgda.Interaction.Highlighting.Generate
highlight_Agda.TypeChecking.Rules.Decl
highMetaPriorityAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Hint 
1 (Type/Class)Agda.Auto.Convert
2 (Data Constructor)Agda.Auto.Convert
hintIsConstructorAgda.Auto.Convert
HintModeAgda.Auto.Syntax
hintQNameAgda.Auto.Convert
HintsAgda.Auto.Options
hitsNotImplementedAgda.Auto.Convert
HMNormalAgda.Auto.Syntax
HMRecCallAgda.Auto.Syntax
HNALConParAgda.Auto.Syntax
HNALConsAgda.Auto.Syntax
HNALNilAgda.Auto.Syntax
HNAppAgda.Auto.Syntax
HNArgListAgda.Auto.Syntax
hnarglistAgda.Auto.Typecheck
hnbAgda.Auto.Typecheck
hncAgda.Auto.Typecheck
HNDoneAgda.Auto.Typecheck
HNExpAgda.Auto.Syntax
HNExp'Agda.Auto.Syntax
HNLamAgda.Auto.Syntax
HNMetaAgda.Auto.Typecheck
hnnAgda.Auto.Typecheck
hnn'Agda.Auto.Typecheck
HNNBlksAgda.Auto.Typecheck
hnn_blksAgda.Auto.Typecheck
hnn_checkstepAgda.Auto.Typecheck
HNPiAgda.Auto.Syntax
HNResAgda.Auto.Typecheck
HNSortAgda.Auto.Syntax
holdConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Hole 
1 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor)Agda.Interaction.Highlighting.Precise
holeAgda.Syntax.Parser.Comments
HoleContent 
1 (Type/Class)Agda.Syntax.Concrete
2 (Type/Class)Agda.Syntax.Abstract
HoleContent'Agda.Syntax.Concrete
HoleContentExprAgda.Syntax.Concrete
holeContentParser 
1 (Function)Agda.Syntax.Parser.Parser
2 (Function)Agda.Syntax.Parser
HoleContentRewriteAgda.Syntax.Concrete
HoleNameAgda.Syntax.Notation
holeNameAgda.Syntax.Notation
holeNumberAgda.Syntax.Common
HolePartAgda.Syntax.Common
holesAgda.Utils.List
holeTargetAgda.Syntax.Notation
hPiAgda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
hPi'Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
hsAppViewAgda.Compiler.MAlonzo.Misc
hsCoerceAgda.Compiler.MAlonzo.Compiler
HsCompileMAgda.Compiler.MAlonzo.Misc
HsCompileState 
1 (Type/Class)Agda.Compiler.MAlonzo.Misc
2 (Data Constructor)Agda.Compiler.MAlonzo.Misc
HsCompileTAgda.Compiler.MAlonzo.Misc
HsDataAgda.Compiler.MAlonzo.Pragmas
HsDefnAgda.Compiler.MAlonzo.Pragmas
hsep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.Pretty
hsepWithAgda.Utils.Pretty
HsExportAgda.Compiler.MAlonzo.Pragmas
hsIntAgda.Compiler.MAlonzo.Misc
hsLambdaAgda.Compiler.MAlonzo.Misc
hsLetAgda.Compiler.MAlonzo.Misc
hslitAgda.Compiler.MAlonzo.Compiler
hsMapAltAgda.Compiler.MAlonzo.Misc
hsMapRHSAgda.Compiler.MAlonzo.Misc
HsModuleEnv 
1 (Type/Class)Agda.Compiler.MAlonzo.Misc
2 (Data Constructor)Agda.Compiler.MAlonzo.Misc
hsNameAgda.Compiler.MAlonzo.Misc
hsOpToExpAgda.Compiler.MAlonzo.Misc
hsPrimOpAgda.Compiler.MAlonzo.Misc
hsPrimOpAppAgda.Compiler.MAlonzo.Misc
hsTelApproximationAgda.Compiler.MAlonzo.HaskellTypes
hsTelApproximation'Agda.Compiler.MAlonzo.HaskellTypes
HsTypeAgda.Compiler.MAlonzo.Pragmas
hsTypedDoubleAgda.Compiler.MAlonzo.Misc
hsTypedIntAgda.Compiler.MAlonzo.Misc
hsVarUQAgda.Compiler.MAlonzo.Misc
htmlBackendAgda.Interaction.Highlighting.HTML
HypAgda.TypeChecking.SizedTypes.WarshallSolver
Hyp'Agda.TypeChecking.SizedTypes.WarshallSolver
hypConnAgda.TypeChecking.SizedTypes.WarshallSolver
HypGraphAgda.TypeChecking.SizedTypes.WarshallSolver
hypGraphAgda.TypeChecking.SizedTypes.WarshallSolver
HypSizeConstraint 
1 (Type/Class)Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Solve