| H | Agda.Auto.Options |
| hackReifyToMeta | Agda.Syntax.Internal |
| handleCommand | Agda.Interaction.InteractionTop |
| handleCommand_ | Agda.Interaction.InteractionTop |
| HandleSol | Agda.Auto.NarrowingSearch |
| hang | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| hasBadRigid | Agda.TypeChecking.MetaVars.Occurs |
| HasBuiltins | Agda.TypeChecking.Monad.Builtin |
| hasCatchAll | Agda.TypeChecking.CompiledClause |
| HasConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasElims | Agda.Syntax.Internal |
| HasEta | Agda.TypeChecking.Datatypes |
| hasExactVerbosity | Agda.TypeChecking.Monad.Options, 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 |
| hashFile | Agda.Utils.Hash |
| HashMap | Agda.Utils.HashMap |
| hashString | Agda.Utils.Hash |
| HashTable | Agda.TypeChecking.Serialise.Base |
| hasInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HaskellCode | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HaskellCodePragma | Agda.Syntax.Concrete |
| HaskellKind | Agda.Compiler.MAlonzo.HaskellTypes |
| HaskellPragma | Agda.Compiler.MAlonzo.Pragmas |
| HaskellType | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| haskellType | Agda.Compiler.MAlonzo.HaskellTypes |
| haskellType' | Agda.Compiler.MAlonzo.HaskellTypes |
| hasLoopingDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasMainFunction | Agda.Compiler.MAlonzo.Primitives |
| HasOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| HasPolarity | Agda.TypeChecking.Polarity |
| HasRange | Agda.Syntax.Position |
| 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.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hasWarnings | Agda.Interaction.Imports |
| HasZero | Agda.Termination.Semiring |
| haveSizedTypes | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| hcat | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| headMaybe | Agda.Utils.List |
| HeadNormal | Agda.Interaction.BasicOps |
| headPrecedence | Agda.Syntax.Fixity |
| headSymbol | Agda.TypeChecking.Injectivity |
| headWithDefault | Agda.Utils.List |
| HellNo | Agda.TypeChecking.InstanceArguments |
| help | Agda.Interaction.CommandLine |
| hequalMetavar | Agda.Auto.NarrowingSearch |
| hexDigit | Agda.Utils.Char |
| 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 |
| hiddenArgumentCtx | Agda.Syntax.Fixity |
| HiddenArgV | Agda.Syntax.Concrete.Operators.Parser |
| HiddenP | Agda.Syntax.Concrete |
| hide | Agda.Syntax.Common |
| hideAndRelParams | Agda.TypeChecking.Irrelevance |
| hideOrKeepInstance | Agda.Syntax.Common |
| Hiding | Agda.Syntax.Common |
| hiding | Agda.Syntax.Common |
| HidingMismatch | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
| highlightAsTypeChecked | Agda.Interaction.Highlighting.Generate |
| highlightExpr | Agda.Interaction.InteractionTop |
| highlightFromInterface | Agda.Interaction.Imports |
| Highlighting | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark |
| HighlightingInfo | 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 |
| 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 |
| 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 | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| hole | Agda.Syntax.Parser.Comments |
| HoleName | Agda.Syntax.Notation |
| holeName | Agda.Syntax.Notation |
| holes | Agda.Utils.List |
| holeTarget | Agda.Syntax.Notation |
| hPi | Agda.TypeChecking.Primitive |
| hPutStr | Agda.Utils.IO.UTF8 |
| hsApp | Agda.Compiler.MAlonzo.HaskellTypes |
| hsAppView | Agda.Compiler.MAlonzo.Misc |
| hsCast | Agda.Compiler.MAlonzo.Compiler |
| hsCast' | Agda.Compiler.MAlonzo.Compiler |
| hsCastApp | Agda.Compiler.MAlonzo.Compiler |
| hsCoerce | Agda.Compiler.MAlonzo.Compiler |
| HsData | Agda.Compiler.MAlonzo.Pragmas |
| HsDefn | Agda.Compiler.MAlonzo.Pragmas |
| hsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| HsExport | Agda.Compiler.MAlonzo.Pragmas |
| hsForall | Agda.Compiler.MAlonzo.HaskellTypes |
| hsFun | Agda.Compiler.MAlonzo.HaskellTypes |
| hsInt | Agda.Compiler.MAlonzo.Misc |
| hsKFun | Agda.Compiler.MAlonzo.HaskellTypes |
| hsLambda | Agda.Compiler.MAlonzo.Misc |
| hsLet | Agda.Compiler.MAlonzo.Misc |
| hslit | Agda.Compiler.MAlonzo.Compiler |
| hsMapAlt | Agda.Compiler.MAlonzo.Misc |
| hsMapRHS | Agda.Compiler.MAlonzo.Misc |
| hsName | Agda.Compiler.MAlonzo.Misc |
| hsOpToExp | Agda.Compiler.MAlonzo.Misc |
| hsPrimOp | Agda.Compiler.MAlonzo.Misc |
| hsPrimOpApp | Agda.Compiler.MAlonzo.Misc |
| hsStar | Agda.Compiler.MAlonzo.HaskellTypes |
| HsType | Agda.Compiler.MAlonzo.Pragmas |
| hsTypedInt | Agda.Compiler.MAlonzo.Misc |
| hsUnit | Agda.Compiler.MAlonzo.HaskellTypes |
| hsVar | Agda.Compiler.MAlonzo.HaskellTypes |
| hsVarUQ | Agda.Compiler.MAlonzo.Misc |
| 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 |