Agda-2.6.0.1: 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

H | Agda.Auto.Options
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
HasBiggerSort | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasBiggerSort | Agda.TypeChecking.Sort
HasBuiltins | Agda.TypeChecking.Monad.Builtin
hasCatchAll | Agda.TypeChecking.CompiledClause
HasConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasCopatterns | Agda.Syntax.Concrete.Pattern
hasElims | Agda.Syntax.Internal
HasEllipsis | Agda.Syntax.Concrete.Pattern
hasEllipsis | Agda.Syntax.Concrete.Pattern
hasEllipsis' | Agda.Syntax.Concrete.Pattern
HasEta | Agda.Syntax.Common
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
HashMap | Agda.Utils.HashMap
hashString | Agda.Utils.Hash
HashTable | Agda.TypeChecking.Serialise.Base
hashText | Agda.Utils.Hash
hashTextFile | Agda.Utils.Hash
hasInputFile | Agda.TypeChecking.Monad.Options, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HaskellCode | Agda.Compiler.MAlonzo.Pragmas
HaskellPragma | Agda.Compiler.MAlonzo.Pragmas
haskellStringLiteral | Agda.Utils.String
HaskellType | Agda.Compiler.MAlonzo.Pragmas
haskellType | Agda.Compiler.MAlonzo.HaskellTypes
hasLoopingDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasMainFunction | Agda.Compiler.MAlonzo.Primitives
hasNoFreeVariables | Agda.Syntax.Common
HasOptions | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasPolarity | Agda.TypeChecking.Polarity
hasProjectionPatterns | Agda.TypeChecking.CompiledClause
HasPTSRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasPTSRule | Agda.TypeChecking.Sort
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
hasWithPatterns | Agda.Syntax.Concrete.Pattern
HasZero | Agda.Termination.Semiring
haveLevels | Agda.TypeChecking.Level
haveSizedTypes | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
haveSizeLt | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hcat |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
headAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
headMaybe | Agda.Utils.List
headNe | Agda.Utils.NonemptyList
HeadNormal | Agda.Interaction.BasicOps
headPrecedence | Agda.Syntax.Fixity
headSymbol | Agda.TypeChecking.Injectivity
headSymbol' | Agda.TypeChecking.Injectivity
headWithDefault | Agda.Utils.List
Help | Agda.Interaction.Options.Help
help | Agda.Interaction.CommandLine
HelpFor | Agda.Interaction.Options.Help
helpTopicUsage | Agda.Interaction.Options.Help
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
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
HighlightAll | Agda.Interaction.Options
highlightAsTypeChecked | Agda.Interaction.Highlighting.Generate
HighlightAuto | Agda.Interaction.Options
HighlightCode | Agda.Interaction.Options
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
HighlightModuleContents | Agda.TypeChecking.Rules.Decl
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
hitsNotImplemented | Agda.Auto.Convert
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
HoleContent |
1 (Type/Class) | Agda.Syntax.Concrete
2 (Type/Class) | Agda.Syntax.Abstract
HoleContent' | Agda.Syntax.Concrete
HoleContentExpr | Agda.Syntax.Concrete
holeContentParser |
1 (Function) | Agda.Syntax.Parser.Parser
2 (Function) | Agda.Syntax.Parser
HoleContentRewrite | Agda.Syntax.Concrete
HoleName | Agda.Syntax.Notation
holeName | Agda.Syntax.Notation
holes | Agda.Utils.List
holeTarget | Agda.Syntax.Notation
hPi | Agda.TypeChecking.Primitive
hPi' | Agda.TypeChecking.Primitive
hPutStr | Agda.Utils.IO.UTF8
hsAppView | Agda.Compiler.MAlonzo.Misc
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
hsInt | Agda.Compiler.MAlonzo.Misc
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
hsTelApproximation | Agda.Compiler.MAlonzo.HaskellTypes
hsTelApproximation' | Agda.Compiler.MAlonzo.HaskellTypes
HsType | Agda.Compiler.MAlonzo.Pragmas
hsTypedInt | Agda.Compiler.MAlonzo.Misc
hsVarUQ | Agda.Compiler.MAlonzo.Misc
HtmlHighlight | Agda.Interaction.Options
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