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 |
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 |
hasLoopingDisplayForm | Agda.TypeChecking.Monad.Signature, Agda.TypeChecking.Monad, Agda.Compiler.Backend |
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 |
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 |
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.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 |
HeadSymbolIsProjection | 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 |
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 |
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 |
HidingOnly | Agda.Syntax.Scope.Base |
hidingToMetaKind | Agda.Syntax.Info |
hidingToString | Agda.Syntax.Common |
highlightAsTypeChecked | Agda.TypeChecking.Monad.Trace, Agda.TypeChecking.Monad, Agda.Interaction.Highlighting.Generate, Agda.Compiler.Backend |
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.TypeChecking.Monad, Agda.Compiler.Backend |
HighlightingMethod | 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 |
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 |