Agda-2.3.2: A dependently typed functional programming language and proof assistant

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- !
- $
- &
- +
- .
- /
- <
- =
- >
- |
- -
- All

Index - H

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