Agda-2.8.0: 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.Mimer.Options
handleCommand | Agda.Interaction.InteractionTop
handleCommand_ | Agda.Interaction.InteractionTop
handleImpossible | Agda.Utils.Impossible
handleImpossibleJust | Agda.Utils.Impossible
hang |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
hasAccessibleDef | Agda.TypeChecking.Opacity
hasAgdaExtension | Agda.Interaction.FindFile
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, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasCallStack | Agda.Utils.CallStack
hasCatchall | Agda.TypeChecking.CompiledClause
HasConstInfo | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasCopatterns | Agda.Syntax.Concrete.Pattern
hasDefP | Agda.Syntax.Internal.Pattern
hasDisplayForms | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.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
hashRawTopLevelModuleName | Agda.Syntax.TopLevelModuleName
hashString | Agda.Utils.Hash
HashTable | Agda.Utils.HashTable
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
hasLineNumber | Agda.Interaction.Library.Base
hasNoFreeVariables | Agda.Syntax.Common
HasOptions | Agda.Interaction.Options, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HasOverlapMode | Agda.Syntax.Common
hasProfileOption | Agda.TypeChecking.Monad.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasProjectionPatterns | Agda.TypeChecking.CompiledClause
HasPTSRule | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasPTSRule | Agda.TypeChecking.Sort
hasQuantity0 | Agda.Syntax.Common
hasQuantity1 | Agda.Syntax.Common
hasQuantityω | Agda.Syntax.Common
HasRange | Agda.Syntax.Position
HasRangeWithoutFile | Agda.Syntax.Position
HasTag | Agda.Utils.BiMap
hasTwinMeta | Agda.TypeChecking.MetaVars
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.Debug, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hasWithPatterns | Agda.Syntax.Concrete.Pattern
HasZero | Agda.Termination.Semiring
haveLevels | Agda.TypeChecking.Level
haveSizeLt | Agda.TypeChecking.Monad.SizedTypes, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hcat |
1 (Function) | Agda.Syntax.Common.Pretty
2 (Function) | Agda.Compiler.JS.Pretty
3 (Function) | Agda.TypeChecking.Pretty
hcomp | Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
HCompOp | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Head | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
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.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
headSymbol | Agda.TypeChecking.Injectivity
headSymbol' | Agda.TypeChecking.Injectivity
HeadSymbolContainsMetas | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HeadSymbolIsProjectionLikeFunction | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HeadSymbolIsTypeConstructor | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
headWithDefault | Agda.Utils.List
Help | Agda.Interaction.Options.Help
help | Agda.Setup.EmacsMode
helpErrors | Agda.Interaction.Options.Errors
HelpFor | Agda.Interaction.Options.Help
helpForLocaleError | Agda.Main
helpTopicUsage | Agda.Interaction.Options.Help
hfill | Agda.TypeChecking.Primitive.Cubical.Base, Agda.TypeChecking.Primitive.Cubical, Agda.TypeChecking.Primitive
Hidden | Agda.Syntax.Common
hidden | Agda.Syntax.Common
HiddenArg | Agda.Syntax.Concrete
HiddenArgV | Agda.Syntax.Concrete.Operators.Parser
HiddenGeneralize | Agda.Syntax.Concrete.Definitions.Errors, Agda.Syntax.Concrete.Definitions
HiddenGeneralize_ | Agda.Interaction.Options.Warnings
HiddenNotInArgumentPosition | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HiddenNotInArgumentPosition_ | Agda.Interaction.Options.Warnings
HiddenP | Agda.Syntax.Concrete
hide | Agda.Syntax.Common
hideAndRelParams | Agda.TypeChecking.Monad.Modality, Agda.TypeChecking.Monad, Agda.Compiler.Backend
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.TypeChecking.Monad, Agda.Compiler.Backend
HidingMismatch_ | Agda.Interaction.Options.Errors
HidingOnly | Agda.Syntax.Scope.Base
hidingToMetaKind | Agda.Syntax.Info
hidingToString | Agda.Syntax.Common
HighlightAll | Agda.Interaction.Highlighting.HTML.Base
highlightAsTypeChecked | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend
HighlightAuto | Agda.Interaction.Highlighting.HTML.Base
HighlightCode | Agda.Interaction.Highlighting.HTML.Base
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.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HighlightingMethod | Agda.TypeChecking.Monad.Base.Types, Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
HighlightModuleContents | Agda.TypeChecking.Rules.Decl
highlightWarning | Agda.Interaction.Highlighting.Generate
highlight_ | Agda.TypeChecking.Rules.Decl
highMetaPriority | Agda.TypeChecking.Monad.Base, Agda.TypeChecking.Monad, Agda.Compiler.Backend
hintExprToQName | Agda.Mimer.Options
HintMode | Agda.Mimer.Options
hlComment | Agda.Syntax.Common.Pretty
hlHole | Agda.Syntax.Common.Pretty
hlKeyword | Agda.Syntax.Common.Pretty
hlNumber | Agda.Syntax.Common.Pretty
hlPragma | Agda.Syntax.Common.Pretty
hlPrimitiveType | Agda.Syntax.Common.Pretty
hlString | Agda.Syntax.Common.Pretty
hlSymbol | Agda.Syntax.Common.Pretty
holdConstraints | Agda.TypeChecking.Monad.Constraints, Agda.TypeChecking.Monad, Agda.Compiler.Backend
Hole |
1 (Data Constructor) | Agda.Syntax.Common.Aspect, Agda.Interaction.Highlighting.Precise
2 (Data Constructor) | 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
holeNumber | Agda.Syntax.Common
HolePart | Agda.Syntax.Common
holes | Agda.Utils.List
holeTarget | Agda.Syntax.Notation
hPi | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
hPi' | Agda.TypeChecking.Primitive.Base, Agda.TypeChecking.Primitive
hsAppView | Agda.Compiler.MAlonzo.Misc
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.Syntax.Common.Pretty
2 (Function) | Agda.TypeChecking.Pretty
hsepWith | Agda.Syntax.Common.Pretty
HsExport | Agda.Compiler.MAlonzo.Pragmas
hsInt | Agda.Compiler.MAlonzo.Misc
hsLambda | Agda.Compiler.MAlonzo.Misc
hsLet | Agda.Compiler.MAlonzo.Misc
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.Backend, Agda.Interaction.Highlighting.HTML
HtmlHighlight | Agda.Interaction.Highlighting.HTML.Base
htmlOptCssFile | Agda.Interaction.Highlighting.HTML.Base
htmlOptDir | Agda.Interaction.Highlighting.HTML.Base
htmlOptHighlight | Agda.Interaction.Highlighting.HTML.Base
htmlOptHighlightOccurrences | Agda.Interaction.Highlighting.HTML.Base
HtmlOptions |
1 (Type/Class) | Agda.Interaction.Highlighting.HTML.Base
2 (Data Constructor) | Agda.Interaction.Highlighting.HTML.Base
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.Syntax
2 (Data Constructor) | Agda.TypeChecking.SizedTypes.Syntax