Agda-2.6.1.3: 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
hasCatchAllAgda.TypeChecking.CompiledClause
HasConstInfoAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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
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
hashStringAgda.Utils.Hash
HashTableAgda.TypeChecking.Serialise.Base
hashTextAgda.Utils.Hash
hashTextFileAgda.Utils.Hash
hasInputFileAgda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HaskellCodeAgda.Compiler.MAlonzo.Pragmas
HaskellPragmaAgda.Compiler.MAlonzo.Pragmas
haskellStringLiteralAgda.Utils.String
HaskellTypeAgda.Compiler.MAlonzo.Pragmas
haskellTypeAgda.Compiler.MAlonzo.HaskellTypes
hasLeftAdjointAgda.Utils.POMonoid
hasLoopingDisplayFormAgda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasMainFunctionAgda.Compiler.MAlonzo.Primitives
hasNoFreeVariablesAgda.Syntax.Common
HasOptionsAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasPolarityAgda.TypeChecking.Polarity
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
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
hasWarningsAgda.Interaction.Imports
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.TypeChecking.Pretty
HeadAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
headAmbQAgda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
HeadNormalAgda.Interaction.Base
headPrecedenceAgda.Syntax.Fixity
headStopAgda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
headSymbolAgda.TypeChecking.Injectivity
headSymbol'Agda.TypeChecking.Injectivity
headWithDefaultAgda.Utils.List
HelpAgda.Interaction.Options.Help
helpAgda.Interaction.CommandLine
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
HidingMismatchAgda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HidingOnlyAgda.Syntax.Scope.Base
HighlightAllAgda.Interaction.Options
highlightAsTypeCheckedAgda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
HighlightAutoAgda.Interaction.Options
HighlightCodeAgda.Interaction.Options
highlightExprAgda.Interaction.InteractionTop
highlightFromInterfaceAgda.Interaction.Imports
HighlightingAgda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
HighlightingInfoAgda.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
HoleAgda.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
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
HsDataAgda.Compiler.MAlonzo.Pragmas
HsDefnAgda.Compiler.MAlonzo.Pragmas
hsep 
1 (Function)Agda.Utils.Pretty
2 (Function)Agda.TypeChecking.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
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
HtmlHighlightAgda.Interaction.Options
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