| handleParseException | Agda.Interaction.Exceptions |
| HandleSol | Agda.Auto.NarrowingSearch |
| hang | Agda.Utils.Pretty |
| hasBadRigid | Agda.TypeChecking.MetaVars.Occurs |
| hasCompiledData | Agda.Compiler.MAlonzo.Primitives |
| HasFresh | Agda.Utils.Fresh |
| hash | Agda.Utils.Hash |
| HashMap | Agda.Utils.HashMap |
| hasInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
| HaskellCode | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellKind | Agda.Compiler.HaskellTypes |
| haskellKind | Agda.Compiler.HaskellTypes |
| HaskellRepresentation | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HaskellType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| haskellType | Agda.Compiler.HaskellTypes |
| 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 |
| HasZero | Agda.Termination.Semiring |
| haveSizedTypes | Agda.TypeChecking.SizedTypes |
| hcat | Agda.Utils.Pretty |
| head'' | Agda.Compiler.Epic.Primitive |
| HeadNormal | Agda.Interaction.BasicOps |
| headSymbol | Agda.TypeChecking.Injectivity |
| help | Agda.Interaction.CommandLine.CommandLine |
| hequalMetavar | Agda.Auto.NarrowingSearch |
| Here | Agda.TypeChecking.Positivity |
| here | Agda.TypeChecking.Positivity |
| Het | Agda.TypeChecking.Rules.LHS.Unify |
| 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 |
| Hiding | |
| 1 (Type/Class) | Agda.Syntax.Common |
| 2 (Data Constructor) | Agda.Syntax.Concrete |
| highlightAsTypeChecked | Agda.Interaction.Highlighting.Generate |
| highlightFromInterface | Agda.Interaction.Imports |
| HighlightingInfo | Agda.Interaction.Highlighting.Precise |
| HighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| HighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| 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 |
| Hole | |
| 1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete |
| 2 (Data Constructor) | Agda.Syntax.Internal.Pattern |
| hole | Agda.Syntax.Parser.Comments |
| HoleName | Agda.Syntax.Notation |
| holeName | Agda.Syntax.Notation |
| holes | Agda.Utils.List |
| holeTarget | Agda.Syntax.Notation |
| Hom | Agda.TypeChecking.Rules.LHS.Unify |
| HomHet | Agda.TypeChecking.Rules.LHS.Unify |
| hPi | Agda.TypeChecking.Primitive |
| hPutStr | Agda.Utils.IO.UTF8 |
| hsApp | Agda.Compiler.HaskellTypes |
| hsCast | Agda.Compiler.MAlonzo.Compiler |
| hsCast' | Agda.Compiler.MAlonzo.Compiler |
| hsCoerce | Agda.Compiler.MAlonzo.Compiler |
| HsDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsep | |
| 1 (Function) | Agda.Utils.Pretty |
| 2 (Function) | Agda.TypeChecking.Pretty |
| hsForall | Agda.Compiler.HaskellTypes |
| hsFun | Agda.Compiler.HaskellTypes |
| hsKFun | Agda.Compiler.HaskellTypes |
| hslit | Agda.Compiler.MAlonzo.Compiler |
| hsStar | Agda.Compiler.HaskellTypes |
| HsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
| hsUnit | Agda.Compiler.HaskellTypes |
| hsVar | Agda.Compiler.HaskellTypes |
| hsVarUQ | Agda.Compiler.MAlonzo.Misc |