| hackReifyToMeta | Agda.Syntax.Internal |
| handleCommand | Agda.Interaction.InteractionTop |
| handleCommand_ | Agda.Interaction.InteractionTop |
| handleParseException | Agda.Interaction.Exceptions |
| HandleSol | Agda.Auto.NarrowingSearch |
| hang | Agda.Utils.Pretty |
| hasBadRigid | Agda.TypeChecking.MetaVars.Occurs |
| HasBuiltins | Agda.TypeChecking.Monad.Builtin |
| hasCatchAll | Agda.TypeChecking.CompiledClause |
| HasConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| hasElims | Agda.Syntax.Internal |
| HasEta | Agda.TypeChecking.Datatypes |
| HasFree | Agda.Compiler.Treeless.Subst |
| HasFresh | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| HaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellCodePragma | Agda.Syntax.Concrete |
| HaskellExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellKind | Agda.Compiler.HaskellTypes |
| HaskellRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| haskellType | Agda.Compiler.HaskellTypes |
| hasLoopingDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad |
| HasOptions | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| HasPolarity | Agda.TypeChecking.Polarity |
| HasRange | Agda.Syntax.Position |
| HasType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| hasVerbosity | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| hasWarnings | Agda.Interaction.Imports |
| HasZero | Agda.Termination.Semiring |
| haveSizedTypes | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad |
| hcat | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| headMaybe | Agda.Utils.List |
| HeadNormal | Agda.Interaction.BasicOps |
| headSymbol | Agda.TypeChecking.Injectivity |
| headWithDefault | Agda.Utils.List |
| help | Agda.Interaction.CommandLine |
| hequalMetavar | Agda.Auto.NarrowingSearch |
| HeterogeneousEquality | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hexDigit | Agda.Utils.Char |
| HI | |
| 1 (Type/Class) | Agda.Auto.CaseSplit |
| 2 (Data Constructor) | Agda.Auto.CaseSplit |
| Hidden | |
| 1 (Data Constructor) | Agda.Auto.Syntax |
| 2 (Data Constructor) | Agda.Syntax.Common |
| HiddenArg | Agda.Syntax.Concrete |
| hiddenArgumentCtx | Agda.Syntax.Fixity |
| HiddenArgV | Agda.Syntax.Concrete.Operators.Parser |
| hiddenFreq | Agda.TypeChecking.Test.Generators |
| HiddenFreqs | |
| 1 (Type/Class) | Agda.TypeChecking.Test.Generators |
| 2 (Data Constructor) | Agda.TypeChecking.Test.Generators |
| hiddenFreqs | Agda.TypeChecking.Test.Generators |
| 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 |
| 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 |
| HighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| highlight_ | Agda.TypeChecking.Rules.Decl |
| highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HintMode | Agda.Auto.Syntax |
| 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 |
| 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 |
| 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.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 |
| HsDataType | |
| 1 (Type/Class) | Agda.Compiler.UHC.MagicTypes |
| 2 (Data Constructor) | Agda.Compiler.UHC.MagicTypes |
| HsDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| HsExport | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsForall | Agda.Compiler.HaskellTypes |
| hsFun | Agda.Compiler.HaskellTypes |
| hsInt | Agda.Compiler.MAlonzo.Misc |
| hsKFun | Agda.Compiler.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.UHC.Bridge, Agda.Compiler.UHC.Pragmas.Base, Agda.Compiler.UHC.Pragmas.Parse |
| hsName | Agda.Compiler.MAlonzo.Misc |
| hsOpToExp | Agda.Compiler.MAlonzo.Misc |
| hspLet | Agda.Compiler.MAlonzo.Misc |
| hsPrimOp | Agda.Compiler.MAlonzo.Misc |
| hsPrimOpApp | Agda.Compiler.MAlonzo.Misc |
| hsStar | Agda.Compiler.HaskellTypes |
| HsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsTypedInt | Agda.Compiler.MAlonzo.Misc |
| HsUnit | Agda.Compiler.UHC.MagicTypes |
| hsUnit | Agda.Compiler.HaskellTypes |
| hsVar | Agda.Compiler.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 |