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

Index - H

HAgda.Mimer.Options
handleCommandAgda.Interaction.InteractionTop
handleCommand_Agda.Interaction.InteractionTop
handleImpossibleAgda.Utils.Impossible
handleImpossibleJustAgda.Utils.Impossible
hang 
1 (Function)Agda.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty
hasAccessibleDefAgda.TypeChecking.Opacity
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
hasDisplayFormsAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
HasOverlapModeAgda.Syntax.Common
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.Syntax.Common.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
HeadSymbolContainsMetasAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HeadSymbolIsProjectionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HeadSymbolIsProjectionLikeFunctionAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HeadSymbolIsTypeConstructorAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
headWithDefaultAgda.Utils.List
HelpAgda.Interaction.Options.Help
HelpForAgda.Interaction.Options.Help
helpForLocaleErrorAgda.Main
helpTopicUsageAgda.Interaction.Options.Help
hfillAgda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
hidingToMetaKindAgda.Syntax.Info
hidingToStringAgda.Syntax.Common
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
hintExprToQNameAgda.Mimer.Options
HintModeAgda.Mimer.Options
hlCommentAgda.Syntax.Common.Pretty
hlHoleAgda.Syntax.Common.Pretty
hlKeywordAgda.Syntax.Common.Pretty
hlNumberAgda.Syntax.Common.Pretty
hlPragmaAgda.Syntax.Common.Pretty
hlPrimitiveTypeAgda.Syntax.Common.Pretty
hlStringAgda.Syntax.Common.Pretty
hlSymbolAgda.Syntax.Common.Pretty
holdConstraintsAgda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Hole 
1 (Data Constructor)Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
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
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.Syntax.Common.Pretty
2 (Function)Agda.TypeChecking.Pretty
hsepWithAgda.Syntax.Common.Pretty
HsExportAgda.Compiler.MAlonzo.Pragmas
hsIntAgda.Compiler.MAlonzo.Misc
hsLambdaAgda.Compiler.MAlonzo.Misc
hsLetAgda.Compiler.MAlonzo.Misc
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.Syntax
2 (Data Constructor)Agda.TypeChecking.SizedTypes.Syntax