Agda-2.6.2.0.20211129: 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.Compiler.Backend, Agda.TypeChecking.Monad
hasBiggerSortAgda.TypeChecking.Sort
HasBuiltinsAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
HasCallStackAgda.Utils.CallStack
hasCatchAllAgda.TypeChecking.CompiledClause
HasConstInfoAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasCopatternsAgda.Syntax.Concrete.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.Compiler.Backend, Agda.TypeChecking.Monad
HasFreeAgda.Compiler.Treeless.Subst
HasFreshAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HashAgda.Utils.Hash
hashByteStringAgda.Utils.Hash
hashStringAgda.Utils.Hash
HashTableAgda.TypeChecking.Serialise.Base
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
hasLoopingDisplayFormAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasNoFreeVariablesAgda.Syntax.Common
HasOptionsAgda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasProjectionPatternsAgda.TypeChecking.CompiledClause
HasPTSRuleAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad
hasUniversePolymorphismAgda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasVerbosityAgda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasWithPatternsAgda.Syntax.Concrete.Pattern
HasZeroAgda.Termination.Semiring
haveLevelsAgda.TypeChecking.Level
haveSizedTypesAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
haveSizeLtAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
hcat 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.Compiler.JS.Pretty
3 (Function)Agda.TypeChecking.Pretty
HeadAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
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, Agda.TypeChecking.Primitive.Cubical
headSymbolAgda.TypeChecking.Injectivity
headSymbol'Agda.TypeChecking.Injectivity
headWithDefaultAgda.Utils.List
HelpAgda.Interaction.Options.Help
HelpForAgda.Interaction.Options.Help
helpTopicUsageAgda.Interaction.Options.Help
hequalMetavarAgda.Auto.NarrowingSearch
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
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.Compiler.Backend, Agda.TypeChecking.Monad
HidingOnlyAgda.Syntax.Scope.Base
highlightAsTypeCheckedAgda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace, Agda.Interaction.Highlighting.Generate
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.Compiler.Backend, Agda.TypeChecking.Monad
HighlightingMethodAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HighlightModuleContentsAgda.TypeChecking.Rules.Decl
highlightWarningAgda.Interaction.Highlighting.Generate
highlight_Agda.TypeChecking.Rules.Decl
highMetaPriorityAgda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
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
holesAgda.Utils.List
holeTargetAgda.Syntax.Notation
hPiAgda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
hPi'Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
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