| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| hasBiggerSort | Agda.TypeChecking.Sort |
| HasBuiltins | Agda.TypeChecking.Monad.Builtin, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HasCallStack | Agda.Utils.CallStack |
| hasCatchAll | Agda.TypeChecking.CompiledClause |
| HasConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HasFree | Agda.Compiler.Treeless.Subst |
| HasFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasNoFreeVariables | Agda.Syntax.Common |
| HasOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasProfileOption | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasProjectionPatterns | Agda.TypeChecking.CompiledClause |
| HasPTSRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasVerbosity | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasWithPatterns | Agda.Syntax.Concrete.Pattern |
| HasZero | Agda.Termination.Semiring |
| haveLevels | Agda.TypeChecking.Level |
| haveSizedTypes | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| haveSizeLt | Agda.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 |
| hcomp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| HCompOp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| Head | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| 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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| headSymbol | Agda.TypeChecking.Injectivity |
| headSymbol' | Agda.TypeChecking.Injectivity |
| HeadSymbolIsProjection | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HeadSymbolIsProjectionLikeFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HeadSymbolNotPostulateFunctionConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive |
| 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.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| HidingOnly | Agda.Syntax.Scope.Base |
| hidingToString | Agda.Syntax.Common |
| highlightAsTypeChecked | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend |
| 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.TypeChecking.Monad, Agda.Compiler.Backend |
| HighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HighlightModuleContents | Agda.TypeChecking.Rules.Decl |
| highlightWarning | Agda.Interaction.Highlighting.Generate |
| highlight_ | Agda.TypeChecking.Rules.Decl |
| highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| 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.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 |
| 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.Base, Agda.TypeChecking.Primitive |
| hPi' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive |
| 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 |