handleAbort | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
handleParseException | Agda.Interaction.Exceptions, Agda.Interaction.GhciTop |
HandlePartSol | Agda.Auto.NarrowingSearch |
HandleSol | Agda.Auto.NarrowingSearch |
hang | Agda.Utils.Pretty |
hasCompiledData | Agda.Compiler.MAlonzo.Primitives |
HasFresh | Agda.Utils.Fresh |
hash | Agda.Utils.Hash |
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 |
HasMeta | Agda.TypeChecking.MetaVars, Agda.Interaction.GhciTop |
HasPolarity | Agda.TypeChecking.Polarity |
HasRange | Agda.Syntax.Position, Agda.Interaction.GhciTop |
HasType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad |
haveSizedTypes | Agda.TypeChecking.SizedTypes |
hcat | Agda.Utils.Pretty |
Head | Agda.Syntax.Abstract.Views |
HeadCon | Agda.Syntax.Abstract.Views |
HeadDef | Agda.Syntax.Abstract.Views |
HeadNormal | Agda.Interaction.BasicOps |
headSymbol | Agda.TypeChecking.Injectivity |
headToExpr | Agda.Syntax.Abstract.Views |
HeadVar | Agda.Syntax.Abstract.Views |
help | Agda.Interaction.CommandLine.CommandLine |
hequalMetavar | Agda.Auto.NarrowingSearch |
Here | |
1 (Data Constructor) | Agda.TypeChecking.Positivity |
2 (Data Constructor) | Agda.TypeChecking.With |
here | Agda.TypeChecking.Positivity |
hexDigit | Agda.Utils.Char |
hGetContents | Agda.Utils.IO.Locale |
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 |
Hiding | |
1 (Type/Class) | Agda.Syntax.Common |
2 (Data Constructor) | Agda.Syntax.Concrete |
HighlightingInfo | Agda.Interaction.Highlighting.Precise |
highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
hn' | Agda.Auto.Typecheck |
HNALConPar | Agda.Auto.Syntax |
HNALCons | Agda.Auto.Syntax |
HNALNil | Agda.Auto.Syntax |
HNApp | Agda.Auto.Syntax |
HNArgList | Agda.Auto.Syntax |
hnarglist | Agda.Auto.Typecheck |
hnc | Agda.Auto.Typecheck |
HNDone | Agda.Auto.Typecheck |
HNExp | Agda.Auto.Syntax |
HNFun | Agda.Auto.Syntax |
HNLam | Agda.Auto.Syntax |
HNMeta | Agda.Auto.Typecheck |
hnn | Agda.Auto.Typecheck |
hnn' | 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 |
holes | Agda.Utils.List |
hPi | Agda.TypeChecking.Primitive |
hsAp | Agda.Compiler.Alonzo.Haskell |
hsApp | Agda.Compiler.HaskellTypes |
hsCast | |
1 (Function) | Agda.Compiler.Alonzo.Haskell |
2 (Function) | Agda.Compiler.MAlonzo.Compiler |
hsCast' | Agda.Compiler.MAlonzo.Compiler |
hsCon | Agda.Compiler.Alonzo.Haskell |
HsDefn | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
hsep | |
1 (Function) | Agda.Utils.Pretty |
2 (Function) | Agda.TypeChecking.Pretty |
hsError | Agda.Compiler.Alonzo.Haskell |
hsForall | Agda.Compiler.HaskellTypes |
hsFun | Agda.Compiler.HaskellTypes |
hsImport | Agda.Compiler.Alonzo.Haskell |
hsKFun | Agda.Compiler.HaskellTypes |
hsLam | Agda.Compiler.Alonzo.Haskell |
hslit | Agda.Compiler.MAlonzo.Compiler |
hsModule | Agda.Compiler.Alonzo.Haskell |
hsModuleImporting | Agda.Compiler.Alonzo.Haskell |
hsPreludeName | Agda.Compiler.Alonzo.Haskell |
hsPreludeTypedExp | Agda.Compiler.Alonzo.Haskell |
hsQImport | Agda.Compiler.Alonzo.Haskell |
hsStar | Agda.Compiler.HaskellTypes |
HsType | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad |
hsTypedExp | Agda.Compiler.Alonzo.Haskell |
hsUndefined | Agda.Compiler.Alonzo.Haskell |
hsVar | |
1 (Function) | Agda.Compiler.Alonzo.Haskell |
2 (Function) | Agda.Compiler.HaskellTypes |
hsVarUQ | Agda.Compiler.MAlonzo.Misc |