A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
:
!
#
$
%
&
+
.
/
<
=
>
?
@
\
^
|
-
_
All

Index - H

H	Agda.Auto.Options
handleCommand	Agda.Interaction.InteractionTop
handleCommand_	Agda.Interaction.InteractionTop
handleImpossible	Agda.Utils.Impossible
handleImpossibleJust	Agda.Utils.Impossible
HandleSol	Agda.Auto.NarrowingSearch
hang
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
hasAccessibleDef	Agda.TypeChecking.Opacity
hasBadRigid	Agda.TypeChecking.MetaVars.Occurs
HasBiggerSort	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasBiggerSort	Agda.TypeChecking.Sort
HasBuiltins	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
HasCallStack	Agda.Utils.CallStack
hasCatchAll	Agda.TypeChecking.CompiledClause
HasConstInfo	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasCopatterns	Agda.Syntax.Concrete.Pattern
hasDefP	Agda.Syntax.Internal.Pattern
hasElem	Agda.Utils.List
hasElims	Agda.Syntax.Internal
HasEllipsis	Agda.Syntax.Concrete.Pattern
hasEllipsis	Agda.Syntax.Concrete.Pattern
hasEllipsis'	Agda.Syntax.Concrete.Pattern
HasEta	Agda.Syntax.Common
HasEta'	Agda.Syntax.Common
HasEta0	Agda.Syntax.Common
hasExactVerbosity	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Debug
HasFree	Agda.Compiler.Treeless.Subst
HasFresh	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Hash	Agda.Utils.Hash
hashByteString	Agda.Utils.Hash
hashRawTopLevelModuleName	Agda.Syntax.TopLevelModuleName
hashString	Agda.Utils.Hash
HashTable	Agda.Utils.HashTable
hashText	Agda.Utils.Hash
hashTextFile	Agda.Utils.Hash
HaskellCode	Agda.Compiler.MAlonzo.Pragmas
HaskellPragma	Agda.Compiler.MAlonzo.Pragmas
haskellStringLiteral	Agda.Utils.String
HaskellType	Agda.Compiler.MAlonzo.Pragmas
haskellType	Agda.Compiler.MAlonzo.HaskellTypes
hasLeftAdjoint	Agda.Utils.POMonoid
hasLineNumber	Agda.Interaction.Library.Base
hasLoopingDisplayForm	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasNoFreeVariables	Agda.Syntax.Common
HasOptions	Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasProfileOption	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Debug
hasProjectionPatterns	Agda.TypeChecking.CompiledClause
HasPTSRule	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasPTSRule	Agda.TypeChecking.Sort
hasQuantity0	Agda.Syntax.Common
hasQuantity1	Agda.Syntax.Common
hasQuantityω	Agda.Syntax.Common
HasRange	Agda.Syntax.Position
HasTag	Agda.Utils.BiMap
hasTwinMeta	Agda.TypeChecking.MetaVars
HasType	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasUniversePolymorphism	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Options
hasVerbosity	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Debug
hasWithPatterns	Agda.Syntax.Concrete.Pattern
HasZero	Agda.Termination.Semiring
haveLevels	Agda.TypeChecking.Level
haveSizedTypes	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
haveSizeLt	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
hcat
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.Compiler.JS.Pretty
3 (Function)	Agda.TypeChecking.Pretty
hcomp	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
HCompOp	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Base
Head	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Base
head
1 (Function)	Agda.Utils.List1
2 (Function)	Agda.Utils.List2
headAmbQ	Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
headCallSite	Agda.Utils.CallStack
HeadCompute	Agda.Interaction.Base
HeadNormal	Agda.Interaction.Base
headPrecedence	Agda.Syntax.Fixity
headStop	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Base
headSymbol	Agda.TypeChecking.Injectivity
headSymbol'	Agda.TypeChecking.Injectivity
headWithDefault	Agda.Utils.List
Help	Agda.Interaction.Options.Help
HelpFor	Agda.Interaction.Options.Help
helpForLocaleError	Agda.Main
helpTopicUsage	Agda.Interaction.Options.Help
hequalMetavar	Agda.Auto.NarrowingSearch
hfill	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive.Cubical.Base
HI
1 (Type/Class)	Agda.Auto.CaseSplit
2 (Data Constructor)	Agda.Auto.CaseSplit
Hidden	Agda.Syntax.Common
hidden	Agda.Syntax.Common
HiddenArg	Agda.Syntax.Concrete
HiddenArgV	Agda.Syntax.Concrete.Operators.Parser
HiddenGeneralize	Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
HiddenGeneralize_	Agda.Interaction.Options.Warnings
HiddenP	Agda.Syntax.Concrete
hide	Agda.Syntax.Common
hideAndRelParams	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Modality
hideOrKeepInstance	Agda.Syntax.Common
Hiding	Agda.Syntax.Common
hiding	Agda.Syntax.Common
HidingDirective	Agda.Syntax.Concrete
HidingDirective'	Agda.Syntax.Common
HidingMismatch	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HidingOnly	Agda.Syntax.Scope.Base
hidingToString	Agda.Syntax.Common
highlightAsTypeChecked	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace, Agda.Interaction.Highlighting.Generate
highlightExpr	Agda.Interaction.InteractionTop
Highlighting	Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
HighlightingInfo	Agda.Interaction.Highlighting.Precise
HighlightingInfoBuilder	Agda.Interaction.Highlighting.Precise
highlightingInfoBuilderInvariant	Agda.Interaction.Highlighting.Precise
highlightingInfoInvariant	Agda.Interaction.Highlighting.Precise
HighlightingLevel	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HighlightingMethod	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HighlightModuleContents	Agda.TypeChecking.Rules.Decl
highlightWarning	Agda.Interaction.Highlighting.Generate
highlight_	Agda.TypeChecking.Rules.Decl
highMetaPriority	Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Hint
1 (Type/Class)	Agda.Auto.Convert
2 (Data Constructor)	Agda.Auto.Convert
hintIsConstructor	Agda.Auto.Convert
HintMode	Agda.Auto.Syntax
hintQName	Agda.Auto.Convert
Hints	Agda.Auto.Options
hitsNotImplemented	Agda.Auto.Convert
hlComment	Agda.Syntax.Common.Pretty
hlHole	Agda.Syntax.Common.Pretty
hlKeyword	Agda.Syntax.Common.Pretty
hlNumber	Agda.Syntax.Common.Pretty
hlPragma	Agda.Syntax.Common.Pretty
hlPrimitiveType	Agda.Syntax.Common.Pretty
hlString	Agda.Syntax.Common.Pretty
hlSymbol	Agda.Syntax.Common.Pretty
HMNormal	Agda.Auto.Syntax
HMRecCall	Agda.Auto.Syntax
HNALConPar	Agda.Auto.Syntax
HNALCons	Agda.Auto.Syntax
HNALNil	Agda.Auto.Syntax
HNApp	Agda.Auto.Syntax
HNArgList	Agda.Auto.Syntax
hnarglist	Agda.Auto.Typecheck
hnb	Agda.Auto.Typecheck
hnc	Agda.Auto.Typecheck
HNDone	Agda.Auto.Typecheck
HNExp	Agda.Auto.Syntax
HNExp'	Agda.Auto.Syntax
HNLam	Agda.Auto.Syntax
HNMeta	Agda.Auto.Typecheck
hnn	Agda.Auto.Typecheck
hnn'	Agda.Auto.Typecheck
HNNBlks	Agda.Auto.Typecheck
hnn_blks	Agda.Auto.Typecheck
hnn_checkstep	Agda.Auto.Typecheck
HNPi	Agda.Auto.Syntax
HNRes	Agda.Auto.Typecheck
HNSort	Agda.Auto.Syntax
holdConstraints	Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
Hole
1 (Data Constructor)	Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor)	Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
hole	Agda.Syntax.Parser.Comments
HoleContent
1 (Type/Class)	Agda.Syntax.Concrete
2 (Type/Class)	Agda.Syntax.Abstract
HoleContent'	Agda.Syntax.Concrete
HoleContentExpr	Agda.Syntax.Concrete
holeContentParser
1 (Function)	Agda.Syntax.Parser.Parser
2 (Function)	Agda.Syntax.Parser
HoleContentRewrite	Agda.Syntax.Concrete
HoleName	Agda.Syntax.Notation
holeName	Agda.Syntax.Notation
holeNumber	Agda.Syntax.Common
HolePart	Agda.Syntax.Common
holes	Agda.Utils.List
holeTarget	Agda.Syntax.Notation
hPi	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
hPi'	Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
hsAppView	Agda.Compiler.MAlonzo.Misc
HsCompileM	Agda.Compiler.MAlonzo.Misc
HsCompileState
1 (Type/Class)	Agda.Compiler.MAlonzo.Misc
2 (Data Constructor)	Agda.Compiler.MAlonzo.Misc
HsCompileT	Agda.Compiler.MAlonzo.Misc
HsData	Agda.Compiler.MAlonzo.Pragmas
HsDefn	Agda.Compiler.MAlonzo.Pragmas
hsep
1 (Function)	Agda.Syntax.Common.Pretty
2 (Function)	Agda.TypeChecking.Pretty
hsepWith	Agda.Syntax.Common.Pretty
HsExport	Agda.Compiler.MAlonzo.Pragmas
hsInt	Agda.Compiler.MAlonzo.Misc
hsLambda	Agda.Compiler.MAlonzo.Misc
hsLet	Agda.Compiler.MAlonzo.Misc
hsMapAlt	Agda.Compiler.MAlonzo.Misc
hsMapRHS	Agda.Compiler.MAlonzo.Misc
HsModuleEnv
1 (Type/Class)	Agda.Compiler.MAlonzo.Misc
2 (Data Constructor)	Agda.Compiler.MAlonzo.Misc
hsName	Agda.Compiler.MAlonzo.Misc
hsOpToExp	Agda.Compiler.MAlonzo.Misc
hsPrimOp	Agda.Compiler.MAlonzo.Misc
hsPrimOpApp	Agda.Compiler.MAlonzo.Misc
hsTelApproximation	Agda.Compiler.MAlonzo.HaskellTypes
hsTelApproximation'	Agda.Compiler.MAlonzo.HaskellTypes
HsType	Agda.Compiler.MAlonzo.Pragmas
hsTypedDouble	Agda.Compiler.MAlonzo.Misc
hsTypedInt	Agda.Compiler.MAlonzo.Misc
hsVarUQ	Agda.Compiler.MAlonzo.Misc
htmlBackend	Agda.Interaction.Highlighting.HTML
Hyp	Agda.TypeChecking.SizedTypes.WarshallSolver
Hyp'	Agda.TypeChecking.SizedTypes.WarshallSolver
hypConn	Agda.TypeChecking.SizedTypes.WarshallSolver
HypGraph	Agda.TypeChecking.SizedTypes.WarshallSolver
hypGraph	Agda.TypeChecking.SizedTypes.WarshallSolver
HypSizeConstraint
1 (Type/Class)	Agda.TypeChecking.SizedTypes.Solve
2 (Data Constructor)	Agda.TypeChecking.SizedTypes.Solve