Agda-2.6.2.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

H | Agda.Auto.Options
handleCommand | Agda.Interaction.InteractionTop
handleCommand_ | Agda.Interaction.InteractionTop
handleImpossible | Agda.Utils.Impossible
handleImpossibleJust | Agda.Utils.Impossible
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.Compiler.Backend, Agda.TypeChecking.Monad
hasBiggerSort | Agda.TypeChecking.Sort
HasBuiltins | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Builtin
HasCallStack | Agda.Utils.CallStack
hasCatchAll | Agda.TypeChecking.CompiledClause
HasConstInfo | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasCopatterns | Agda.Syntax.Concrete.Pattern
hasElem | Agda.Utils.List
hasElims | Agda.Syntax.Internal
HasEllipsis | Agda.Syntax.Concrete.Pattern
hasEllipsis | Agda.Syntax.Concrete.Pattern
hasEllipsis' | Agda.Syntax.Concrete.Pattern
HasEta | Agda.Syntax.Common
HasEta' | Agda.Syntax.Common
HasEta0 | Agda.Syntax.Common
hasExactVerbosity | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HasFree | Agda.Compiler.Treeless.Subst
HasFresh | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
Hash | Agda.Utils.Hash
hashByteString | Agda.Utils.Hash
hashString | Agda.Utils.Hash
HashTable | Agda.TypeChecking.Serialise.Base
hashText | Agda.Utils.Hash
hashTextFile | Agda.Utils.Hash
HaskellCode | Agda.Compiler.MAlonzo.Pragmas
HaskellPragma | Agda.Compiler.MAlonzo.Pragmas
haskellStringLiteral | Agda.Utils.String
HaskellType | Agda.Compiler.MAlonzo.Pragmas
haskellType | Agda.Compiler.MAlonzo.HaskellTypes
hasLeftAdjoint | Agda.Utils.POMonoid
hasLoopingDisplayForm | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Signature
hasNoFreeVariables | Agda.Syntax.Common
HasOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasProjectionPatterns | Agda.TypeChecking.CompiledClause
HasPTSRule | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasPTSRule | Agda.TypeChecking.Sort
hasQuantity0 | Agda.Syntax.Common
hasQuantity1 | Agda.Syntax.Common
hasQuantityω | Agda.Syntax.Common
HasRange | Agda.Syntax.Position
HasTag | Agda.Utils.BiMap
hasTwinMeta | Agda.TypeChecking.MetaVars
HasType | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasUniversePolymorphism | Agda.TypeChecking.Monad.Options, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasVerbosity | Agda.TypeChecking.Monad.Debug, Agda.Compiler.Backend, Agda.TypeChecking.Monad
hasWithPatterns | Agda.Syntax.Concrete.Pattern
HasZero | Agda.Termination.Semiring
haveLevels | Agda.TypeChecking.Level
haveSizedTypes | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
haveSizeLt | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.SizedTypes
hcat |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
Head | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
head |
1 (Function) | Agda.Utils.List1
2 (Function) | Agda.Utils.List2
headAmbQ | Agda.Syntax.Abstract.Name, Agda.Syntax.Treeless, Agda.Syntax.Internal, Agda.Syntax.Abstract, Agda.Compiler.Backend
headCallSite | Agda.Utils.CallStack
HeadCompute | Agda.Interaction.Base
HeadNormal | Agda.Interaction.Base
headPrecedence | Agda.Syntax.Fixity
headStop | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Cubical
headSymbol | Agda.TypeChecking.Injectivity
headSymbol' | Agda.TypeChecking.Injectivity
headWithDefault | Agda.Utils.List
Help | Agda.Interaction.Options.Help
HelpFor | Agda.Interaction.Options.Help
helpTopicUsage | Agda.Interaction.Options.Help
hequalMetavar | Agda.Auto.NarrowingSearch
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
HidingDirective | Agda.Syntax.Concrete
HidingDirective' | Agda.Syntax.Common
HidingMismatch | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HidingOnly | Agda.Syntax.Scope.Base
highlightAsTypeChecked | Agda.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Trace, Agda.Interaction.Highlighting.Generate
highlightExpr | Agda.Interaction.InteractionTop
Highlighting | Agda.Benchmarking, Agda.TypeChecking.Monad.Benchmark
HighlightingInfo | Agda.Interaction.Highlighting.Precise
HighlightingInfoBuilder | Agda.Interaction.Highlighting.Precise
highlightingInfoBuilderInvariant | Agda.Interaction.Highlighting.Precise
highlightingInfoInvariant | Agda.Interaction.Highlighting.Precise
HighlightingLevel | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HighlightingMethod | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
HighlightModuleContents | Agda.TypeChecking.Rules.Decl
highlightWarning | Agda.Interaction.Highlighting.Generate
highlight_ | Agda.TypeChecking.Rules.Decl
highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.Compiler.Backend, Agda.TypeChecking.Monad
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.Compiler.Backend, Agda.TypeChecking.Monad, Agda.TypeChecking.Monad.Constraints
Hole |
1 (Data Constructor) | Agda.Syntax.Concrete.Name, Agda.Syntax.Concrete
2 (Data Constructor) | Agda.Interaction.Highlighting.Precise
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, Agda.TypeChecking.Primitive.Base
hPi' | Agda.TypeChecking.Primitive, Agda.TypeChecking.Primitive.Base
hsAppView | Agda.Compiler.MAlonzo.Misc
hsCoerce | Agda.Compiler.MAlonzo.Compiler
HsCompileM | Agda.Compiler.MAlonzo.Misc
HsCompileState |
1 (Type/Class) | Agda.Compiler.MAlonzo.Misc
2 (Data Constructor) | Agda.Compiler.MAlonzo.Misc
HsCompileT | Agda.Compiler.MAlonzo.Misc
HsData | Agda.Compiler.MAlonzo.Pragmas
HsDefn | Agda.Compiler.MAlonzo.Pragmas
hsep |
1 (Function) | Agda.Utils.Pretty
2 (Function) | Agda.TypeChecking.Pretty
hsepWith | Agda.Utils.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
HsModuleEnv |
1 (Type/Class) | Agda.Compiler.MAlonzo.Misc
2 (Data Constructor) | 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
hsTypedDouble | Agda.Compiler.MAlonzo.Misc
hsTypedInt | Agda.Compiler.MAlonzo.Misc
hsVarUQ | Agda.Compiler.MAlonzo.Misc
htmlBackend | Agda.Interaction.Highlighting.HTML
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