Agda.TypeChecking.Pretty

Documentation

newtype PrettyContext

Constructors

PrettyContext Context

Instances

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => PrettyContext -> m Doc

class PrettyTCM a where

Methods

prettyTCM :: MonadPretty m => a -> m Doc

Instances

PrettyTCM Expr

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Expr -> m Doc

PrettyTCM ProblemEq

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => ProblemEq -> m Doc

PrettyTCM TypedBinding

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TypedBinding -> m Doc

PrettyTCM ModuleName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ModuleName -> m Doc

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Name -> m Doc

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QName -> m Doc

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MetaId -> m Doc

PrettyTCM Modality

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Modality -> m Doc

PrettyTCM Nat

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Nat -> m Doc

PrettyTCM ProblemId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ProblemId -> m Doc

PrettyTCM Quantity

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Quantity -> m Doc

PrettyTCM Relevance

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Relevance -> m Doc

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Name -> m Doc

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QName -> m Doc

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Clause -> m Doc

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ConHead -> m Doc

PrettyTCM DBPatVar

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => DBPatVar -> m Doc

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim -> m Doc

PrettyTCM EqualityView

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => EqualityView -> m Doc

PrettyTCM Level

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Level -> m Doc

PrettyTCM Sort

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Sort -> m Doc

PrettyTCM Telescope

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Telescope -> m Doc

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Term -> m Doc

PrettyTCM Type

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Type -> m Doc

PrettyTCM Blocker

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Blocker -> m Doc

PrettyTCM Literal

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Literal -> m Doc

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Range -> m Doc

PrettyTCM AbstractName

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => AbstractName -> m Doc

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedClause -> m Doc

PrettyTCM SplitClause

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: MonadPretty m => SplitClause -> m Doc

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

prettyTCM :: MonadPretty m => SplitPatVar -> m Doc

PrettyTCM SplitTag

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => SplitTag -> m Doc

PrettyTCM Call

Defined in Agda.TypeChecking.Pretty.Call

Methods

prettyTCM :: MonadPretty m => Call -> m Doc

PrettyTCM CallInfo

Defined in Agda.TypeChecking.Pretty.Call

Methods

prettyTCM :: MonadPretty m => CallInfo -> m Doc

PrettyTCM Candidate

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Candidate -> m Doc

PrettyTCM CheckpointId

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => CheckpointId -> m Doc

PrettyTCM CompareAs

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => CompareAs -> m Doc

PrettyTCM Comparison

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Comparison -> m Doc

PrettyTCM Constraint

Defined in Agda.TypeChecking.Pretty.Constraint

Methods

prettyTCM :: MonadPretty m => Constraint -> m Doc

PrettyTCM DisplayTerm

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => DisplayTerm -> m Doc

PrettyTCM IsForced

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => IsForced -> m Doc

PrettyTCM NLPSort

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NLPSort -> m Doc

PrettyTCM NLPType

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NLPType -> m Doc

PrettyTCM NLPat

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NLPat -> m Doc

PrettyTCM NegativeUnification

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => NegativeUnification -> m Doc

PrettyTCM Polarity

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Polarity -> m Doc

PrettyTCM ProblemConstraint

Defined in Agda.TypeChecking.Pretty.Constraint

Methods

prettyTCM :: MonadPretty m => ProblemConstraint -> m Doc

PrettyTCM RewriteRule

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => RewriteRule -> m Doc

PrettyTCM SplitError

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => SplitError -> m Doc

PrettyTCM TCErr

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => TCErr -> m Doc

PrettyTCM TCWarning

Defined in Agda.TypeChecking.Pretty.Warning

Methods

prettyTCM :: MonadPretty m => TCWarning -> m Doc

PrettyTCM TypeCheckingProblem

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => TypeCheckingProblem -> m Doc

PrettyTCM TypeError

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => TypeError -> m Doc

PrettyTCM UnificationFailure

Defined in Agda.TypeChecking.Errors

Methods

prettyTCM :: MonadPretty m => UnificationFailure -> m Doc

PrettyTCM Node

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Node -> m Doc

PrettyTCM Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Occurrence -> m Doc

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => PrettyContext -> m Doc

PrettyTCM ElimType

Defined in Agda.TypeChecking.Records

Methods

prettyTCM :: MonadPretty m => ElimType -> m Doc

PrettyTCM AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc

PrettyTCM AnnotationPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc

PrettyTCM AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AsBinding -> m Doc

PrettyTCM DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => DotPattern -> m Doc

PrettyTCM LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc

PrettyTCM HypSizeConstraint

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc

PrettyTCM SizeConstraint

Assumes we are in the right context.

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: MonadPretty m => SizeConstraint -> m Doc

PrettyTCM SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

prettyTCM :: MonadPretty m => SizeMeta -> m Doc

PrettyTCM ErrorPart

Defined in Agda.TypeChecking.Unquote

Methods

prettyTCM :: MonadPretty m => ErrorPart -> m Doc

PrettyTCM Permutation

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Permutation -> m Doc

PrettyTCM String

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => String -> m Doc

PrettyTCM Bool

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Bool -> m Doc

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QNamed Clause -> m Doc

PrettyTCM (Arg Expr)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Expr -> m Doc

PrettyTCM (Arg Term)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Term -> m Doc

PrettyTCM (Arg Type)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Type -> m Doc

PrettyTCM (Arg Bool)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Bool -> m Doc

PrettyTCM (NamedArg Expr)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc

PrettyTCM (NamedArg Term)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedArg Term -> m Doc

PrettyTCM (Named_ Term)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Named_ Term -> m Doc

PrettyTCM a => PrettyTCM (WithHiding a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => WithHiding a -> m Doc

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Blocked a -> m Doc

PrettyTCM (Dom Type)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom Type -> m Doc

PrettyTCM (Dom (Name, Type))

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom (Name, Type) -> m Doc

PrettyTCM a => PrettyTCM (Pattern' a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern' a -> m Doc

(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Substitution' a -> m Doc

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Type' NLPat -> m Doc

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim' NLPat -> m Doc

PrettyTCM a => PrettyTCM (Masked a)

Print masked things in double parentheses.

Defined in Agda.Termination.Monad

Methods

prettyTCM :: MonadPretty m => Masked a -> m Doc

PrettyTCM a => PrettyTCM (Closure a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Closure a -> m Doc

PrettyTCM a => PrettyTCM (Judgement a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Judgement a -> m Doc

PrettyTCM a => PrettyTCM (MaybeReduced a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => MaybeReduced a -> m Doc

PrettyTCM (LHSState a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LHSState a -> m Doc

PrettyTCM (Seq OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc

PrettyTCM a => PrettyTCM (Maybe a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Maybe a -> m Doc

PrettyTCM a => PrettyTCM [a]

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => [a] -> m Doc

(PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Graph n e -> m Doc

(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Map k v -> m Doc

(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => (a, b) -> m Doc

(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => (a, b, c) -> m Doc

type MonadPretty m = (MonadReify m, MonadAbsToCon m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc

prettyList without the brackets.

pretty :: (Applicative m, Pretty a) => a -> m Doc

nest :: Functor m => Int -> m Doc -> m Doc

($$) :: Applicative m => m Doc -> m Doc -> m Doc infixl 5

(<+>) :: Applicative m => m Doc -> m Doc -> m Doc infixl 6

(<?>) :: Applicative m => m Doc -> m Doc -> m Doc infixl 6

hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc

sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

text :: Applicative m => String -> m Doc

class PrettyTCMWithNode a where

Pretty-print something paired with a (printable) node. | This intermediate typeclass exists to avoid UndecidableInstances.

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc

Instances

PrettyTCMWithNode Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc

PrettyTCMWithNode (Edge OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc

data WithNode n a

Pairing something with a node (for printing only).

Constructors

WithNode n a

type Doc = Doc

comma :: Applicative m => m Doc

colon :: Applicative m => m Doc

equals :: Applicative m => m Doc

prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc

prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc

multiLineText :: Applicative m => String -> m Doc

pwords :: Applicative m => String -> [m Doc]

fwords :: Applicative m => String -> m Doc

hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc

($+$) :: Applicative m => m Doc -> m Doc -> m Doc infixl 5

braces :: Functor m => m Doc -> m Doc

dbraces :: Functor m => m Doc -> m Doc

brackets :: Functor m => m Doc -> m Doc

parens :: Functor m => m Doc -> m Doc

parensNonEmpty :: Functor m => m Doc -> m Doc

doubleQuotes :: Functor m => m Doc -> m Doc

quotes :: Functor m => m Doc -> m Doc

pshow :: (Applicative m, Show a) => a -> m Doc

prettyList :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc

Comma-separated list in brackets.

punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]

prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc

Pretty print with a given context precedence

prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc

prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]

Proper pretty printing of patterns:

prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc

class Semigroup a where

The class of semigroups (types with an associative binary operation).

Instances should satisfy the following:

Associativity

x <> (y <> z) = (x <> y) <> z

Since: base-4.9.0.0

Methods

(<>) :: a -> a -> a infixr 6

An associative operation.

>>> [1,2,3] <> [4,5,6]
[1,2,3,4,5,6]

Instances

Semigroup IsMain

Conjunctive semigroup (NotMain is absorbing).

Defined in Agda.Compiler.Common

Methods

(<>) :: IsMain -> IsMain -> IsMain

sconcat :: NonEmpty IsMain -> IsMain

stimes :: Integral b => b -> IsMain -> IsMain

Semigroup Doc

Defined in Agda.Compiler.JS.Pretty

Methods

(<>) :: Doc -> Doc -> Doc

sconcat :: NonEmpty Doc -> Doc

stimes :: Integral b => b -> Doc -> Doc

Semigroup Comment

Defined in Agda.Compiler.JS.Syntax

Methods

(<>) :: Comment -> Comment -> Comment

sconcat :: NonEmpty Comment -> Comment

stimes :: Integral b => b -> Comment -> Comment

Semigroup UsesFloat

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

(<>) :: UsesFloat -> UsesFloat -> UsesFloat

sconcat :: NonEmpty UsesFloat -> UsesFloat

stimes :: Integral b => b -> UsesFloat -> UsesFloat

Semigroup HsCompileState

Defined in Agda.Compiler.MAlonzo.Misc

Methods

(<>) :: HsCompileState -> HsCompileState -> HsCompileState

sconcat :: NonEmpty HsCompileState -> HsCompileState

stimes :: Integral b => b -> HsCompileState -> HsCompileState

Semigroup Occurs

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: Occurs -> Occurs -> Occurs

sconcat :: NonEmpty Occurs -> Occurs

stimes :: Integral b => b -> Occurs -> Occurs

Semigroup SeqArg

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: SeqArg -> SeqArg -> SeqArg

sconcat :: NonEmpty SeqArg -> SeqArg

stimes :: Integral b => b -> SeqArg -> SeqArg

Semigroup UnderLambda

Defined in Agda.Compiler.Treeless.Subst

Methods

(<>) :: UnderLambda -> UnderLambda -> UnderLambda

sconcat :: NonEmpty UnderLambda -> UnderLambda

stimes :: Integral b => b -> UnderLambda -> UnderLambda

Semigroup Aspect

NameKind in Name can get more precise.

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: Aspect -> Aspect -> Aspect

sconcat :: NonEmpty Aspect -> Aspect

stimes :: Integral b => b -> Aspect -> Aspect

Semigroup Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: Aspects -> Aspects -> Aspects

sconcat :: NonEmpty Aspects -> Aspects

stimes :: Integral b => b -> Aspects -> Aspects

Semigroup DefinitionSite

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite

sconcat :: NonEmpty DefinitionSite -> DefinitionSite

stimes :: Integral b => b -> DefinitionSite -> DefinitionSite

Semigroup NameKind

Some NameKinds are more informative than others.

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: NameKind -> NameKind -> NameKind

sconcat :: NonEmpty NameKind -> NameKind

stimes :: Integral b => b -> NameKind -> NameKind

Semigroup PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: PositionMap -> PositionMap -> PositionMap

sconcat :: NonEmpty PositionMap -> PositionMap

stimes :: Integral b => b -> PositionMap -> PositionMap

Semigroup TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: TokenBased -> TokenBased -> TokenBased

sconcat :: NonEmpty TokenBased -> TokenBased

stimes :: Integral b => b -> TokenBased -> TokenBased

Semigroup CoverageCheck

Defined in Agda.Syntax.Common

Methods

(<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck

sconcat :: NonEmpty CoverageCheck -> CoverageCheck

stimes :: Integral b => b -> CoverageCheck -> CoverageCheck

Semigroup ExpandedEllipsis

Defined in Agda.Syntax.Common

Methods

(<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis

sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis

stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis

Semigroup FreeVariables

Defined in Agda.Syntax.Common

Methods

(<>) :: FreeVariables -> FreeVariables -> FreeVariables

sconcat :: NonEmpty FreeVariables -> FreeVariables

stimes :: Integral b => b -> FreeVariables -> FreeVariables

Semigroup Hiding

Hiding is an idempotent partial monoid, with unit NotHidden. Instance and NotHidden are incompatible.

Defined in Agda.Syntax.Common

Methods

(<>) :: Hiding -> Hiding -> Hiding

sconcat :: NonEmpty Hiding -> Hiding

stimes :: Integral b => b -> Hiding -> Hiding

Semigroup IsAbstract

Semigroup computes if any of several is an AbstractDef.

Defined in Agda.Syntax.Common

Methods

(<>) :: IsAbstract -> IsAbstract -> IsAbstract

sconcat :: NonEmpty IsAbstract -> IsAbstract

stimes :: Integral b => b -> IsAbstract -> IsAbstract

Semigroup Overlappable

Just for the Hiding instance. Should never combine different overlapping.

Defined in Agda.Syntax.Common

Methods

(<>) :: Overlappable -> Overlappable -> Overlappable

sconcat :: NonEmpty Overlappable -> Overlappable

stimes :: Integral b => b -> Overlappable -> Overlappable

Semigroup PositivityCheck

Defined in Agda.Syntax.Common

Methods

(<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck

sconcat :: NonEmpty PositivityCheck -> PositivityCheck

stimes :: Integral b => b -> PositivityCheck -> PositivityCheck

Semigroup Q0Origin

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Defined in Agda.Syntax.Common

Methods

(<>) :: Q0Origin -> Q0Origin -> Q0Origin

sconcat :: NonEmpty Q0Origin -> Q0Origin

stimes :: Integral b => b -> Q0Origin -> Q0Origin

Semigroup Q1Origin

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Defined in Agda.Syntax.Common

Methods

(<>) :: Q1Origin -> Q1Origin -> Q1Origin

sconcat :: NonEmpty Q1Origin -> Q1Origin

stimes :: Integral b => b -> Q1Origin -> Q1Origin

Semigroup QωOrigin

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Defined in Agda.Syntax.Common

Methods

(<>) :: QωOrigin -> QωOrigin -> QωOrigin

sconcat :: NonEmpty QωOrigin -> QωOrigin

stimes :: Integral b => b -> QωOrigin -> QωOrigin

Semigroup MutualChecks

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

(<>) :: MutualChecks -> MutualChecks -> MutualChecks

sconcat :: NonEmpty MutualChecks -> MutualChecks

stimes :: Integral b => b -> MutualChecks -> MutualChecks

Semigroup PatInfo

Defined in Agda.Syntax.Info

Methods

(<>) :: PatInfo -> PatInfo -> PatInfo

sconcat :: NonEmpty PatInfo -> PatInfo

stimes :: Integral b => b -> PatInfo -> PatInfo

Semigroup Blocker

Defined in Agda.Syntax.Internal.Blockers

Methods

(<>) :: Blocker -> Blocker -> Blocker

sconcat :: NonEmpty Blocker -> Blocker

stimes :: Integral b => b -> Blocker -> Blocker

Semigroup NameMapEntry

Invariant: the KindOfName components should be equal whenever we have to concrete renderings of an abstract name.

Defined in Agda.Syntax.Scope.Base

Methods

(<>) :: NameMapEntry -> NameMapEntry -> NameMapEntry

sconcat :: NonEmpty NameMapEntry -> NameMapEntry

stimes :: Integral b => b -> NameMapEntry -> NameMapEntry

Semigroup CallPath

Defined in Agda.Termination.Monad

Methods

(<>) :: CallPath -> CallPath -> CallPath

sconcat :: NonEmpty CallPath -> CallPath

stimes :: Integral b => b -> CallPath -> CallPath

Semigroup VarCounts

Defined in Agda.TypeChecking.Free

Methods

(<>) :: VarCounts -> VarCounts -> VarCounts

sconcat :: NonEmpty VarCounts -> VarCounts

stimes :: Integral b => b -> VarCounts -> VarCounts

Semigroup FlexRigMap

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: FlexRigMap -> FlexRigMap -> FlexRigMap

sconcat :: NonEmpty FlexRigMap -> FlexRigMap

stimes :: Integral b => b -> FlexRigMap -> FlexRigMap

Semigroup MetaSet

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: MetaSet -> MetaSet -> MetaSet

sconcat :: NonEmpty MetaSet -> MetaSet

stimes :: Integral b => b -> MetaSet -> MetaSet

Semigroup ReduceDefs

Defined in Agda.TypeChecking.Monad.Base

Methods

(<>) :: ReduceDefs -> ReduceDefs -> ReduceDefs

sconcat :: NonEmpty ReduceDefs -> ReduceDefs

stimes :: Integral b => b -> ReduceDefs -> ReduceDefs

Semigroup Simplification

Defined in Agda.TypeChecking.Monad.Base

Methods

(<>) :: Simplification -> Simplification -> Simplification

sconcat :: NonEmpty Simplification -> Simplification

stimes :: Integral b => b -> Simplification -> Simplification

Semigroup OccurrencesBuilder

The semigroup laws only hold up to flattening of Concat.

Defined in Agda.TypeChecking.Positivity

Methods

(<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder

sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder

stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder

Semigroup ClausesPostChecks

Defined in Agda.TypeChecking.Rules.Def

Methods

(<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks

sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks

stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks

Semigroup FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(<>) :: FlexChoice -> FlexChoice -> FlexChoice

sconcat :: NonEmpty FlexChoice -> FlexChoice

stimes :: Integral b => b -> FlexChoice -> FlexChoice

Semigroup LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns

sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns

stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns

Semigroup AbsolutePath

To get Semigroup Range', we need a semigroup instance for AbsolutePath.

Defined in Agda.Syntax.Position

Methods

(<>) :: AbsolutePath -> AbsolutePath -> AbsolutePath

sconcat :: NonEmpty AbsolutePath -> AbsolutePath

stimes :: Integral b => b -> AbsolutePath -> AbsolutePath

Semigroup IntSet

Defined in Agda.Utils.IntSet.Infinite

Methods

(<>) :: IntSet -> IntSet -> IntSet

sconcat :: NonEmpty IntSet -> IntSet

stimes :: Integral b => b -> IntSet -> IntSet

Semigroup MaxNat

Defined in Agda.Utils.Monoid

Methods

(<>) :: MaxNat -> MaxNat -> MaxNat

sconcat :: NonEmpty MaxNat -> MaxNat

stimes :: Integral b => b -> MaxNat -> MaxNat

Semigroup PartialOrdering

Partial ordering forms a monoid under sequencing.

Defined in Agda.Utils.PartialOrd

Methods

(<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering

sconcat :: NonEmpty PartialOrdering -> PartialOrdering

stimes :: Integral b => b -> PartialOrdering -> PartialOrdering

Semigroup All

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: All -> All -> All

sconcat :: NonEmpty All -> All

stimes :: Integral b => b -> All -> All

Semigroup Any

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Any -> Any -> Any

sconcat :: NonEmpty Any -> Any

stimes :: Integral b => b -> Any -> Any

Semigroup Void

Since: base-4.9.0.0

Defined in Data.Void

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Semigroup Attribute

Defined in Text.Blaze.Internal

Methods

(<>) :: Attribute -> Attribute -> Attribute

sconcat :: NonEmpty Attribute -> Attribute

stimes :: Integral b => b -> Attribute -> Attribute

Semigroup AttributeValue

Defined in Text.Blaze.Internal

Methods

(<>) :: AttributeValue -> AttributeValue -> AttributeValue

sconcat :: NonEmpty AttributeValue -> AttributeValue

stimes :: Integral b => b -> AttributeValue -> AttributeValue

Semigroup ChoiceString

Defined in Text.Blaze.Internal

Methods

(<>) :: ChoiceString -> ChoiceString -> ChoiceString

sconcat :: NonEmpty ChoiceString -> ChoiceString

stimes :: Integral b => b -> ChoiceString -> ChoiceString

Semigroup Builder

Defined in Data.ByteString.Builder.Internal

Methods

(<>) :: Builder -> Builder -> Builder

sconcat :: NonEmpty Builder -> Builder

stimes :: Integral b => b -> Builder -> Builder

Semigroup ByteString

Defined in Data.ByteString.Internal

Methods

(<>) :: ByteString -> ByteString -> ByteString

sconcat :: NonEmpty ByteString -> ByteString

stimes :: Integral b => b -> ByteString -> ByteString

Semigroup ByteString

Defined in Data.ByteString.Lazy.Internal

Methods

(<>) :: ByteString -> ByteString -> ByteString

sconcat :: NonEmpty ByteString -> ByteString

stimes :: Integral b => b -> ByteString -> ByteString

Semigroup ShortByteString

Defined in Data.ByteString.Short.Internal

Methods

(<>) :: ShortByteString -> ShortByteString -> ShortByteString

sconcat :: NonEmpty ShortByteString -> ShortByteString

stimes :: Integral b => b -> ShortByteString -> ShortByteString

Semigroup IntSet

Since: containers-0.5.7

Defined in Data.IntSet.Internal

Methods

(<>) :: IntSet -> IntSet -> IntSet

sconcat :: NonEmpty IntSet -> IntSet

stimes :: Integral b => b -> IntSet -> IntSet

Semigroup Ordering

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: Ordering -> Ordering -> Ordering

sconcat :: NonEmpty Ordering -> Ordering

stimes :: Integral b => b -> Ordering -> Ordering

Semigroup Slot

Defined in Data.HashTable.ST.Basic

Methods

(<>) :: Slot -> Slot -> Slot

sconcat :: NonEmpty Slot -> Slot

stimes :: Integral b => b -> Slot -> Slot

Semigroup Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

(<>) :: Doc -> Doc -> Doc

sconcat :: NonEmpty Doc -> Doc

stimes :: Integral b => b -> Doc -> Doc

Semigroup ByteArray

Defined in Data.Primitive.ByteArray

Methods

(<>) :: ByteArray -> ByteArray -> ByteArray

sconcat :: NonEmpty ByteArray -> ByteArray

stimes :: Integral b => b -> ByteArray -> ByteArray

Semigroup Series

Defined in Data.Aeson.Encoding.Internal

Methods

(<>) :: Series -> Series -> Series

sconcat :: NonEmpty Series -> Series

stimes :: Integral b => b -> Series -> Series

Semigroup Key

Defined in Data.Aeson.Key

Methods

(<>) :: Key -> Key -> Key

sconcat :: NonEmpty Key -> Key

stimes :: Integral b => b -> Key -> Key

Semigroup CalendarDiffDays

Additive

Defined in Data.Time.Calendar.CalendarDiffDays

Methods

(<>) :: CalendarDiffDays -> CalendarDiffDays -> CalendarDiffDays

sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays

stimes :: Integral b => b -> CalendarDiffDays -> CalendarDiffDays

Semigroup CalendarDiffTime

Additive

Defined in Data.Time.LocalTime.Internal.CalendarDiffTime

Methods

(<>) :: CalendarDiffTime -> CalendarDiffTime -> CalendarDiffTime

sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime

stimes :: Integral b => b -> CalendarDiffTime -> CalendarDiffTime

Semigroup More

Defined in Data.Attoparsec.Internal.Types

Methods

(<>) :: More -> More -> More

sconcat :: NonEmpty More -> More

stimes :: Integral b => b -> More -> More

Semigroup ShortText

Defined in Data.Text.Short.Internal

Methods

(<>) :: ShortText -> ShortText -> ShortText

sconcat :: NonEmpty ShortText -> ShortText

stimes :: Integral b => b -> ShortText -> ShortText

Semigroup ()

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: () -> () -> ()

sconcat :: NonEmpty () -> ()

stimes :: Integral b => b -> () -> ()

Semigroup (DelayedMerge hl)

Defined in Agda.Interaction.Highlighting.Precise

Methods

(<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl

sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl

stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl

Semigroup (UnderAddition Cohesion)

Cohesion forms a semigroup under addition.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion

sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion

stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion

Semigroup (UnderAddition Modality)

Pointwise addition.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality

sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality

stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality

Semigroup (UnderAddition Quantity)

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity

sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity

stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity

Semigroup (UnderAddition Relevance)

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance

sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance

stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance

Semigroup (UnderComposition Cohesion)

Cohesion forms a semigroup under composition.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion

sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion

stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion

Semigroup (UnderComposition Erased)

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased

sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased

stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased

Semigroup (UnderComposition Modality)

Pointwise composition.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality

sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality

stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality

Semigroup (UnderComposition Quantity)

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity

sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity

stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity

Semigroup (UnderComposition Relevance)

Relevance forms a semigroup under composition.

Defined in Agda.Syntax.Common

Methods

(<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance

sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance

stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance

Semigroup (NotBlocked' t)

ReallyNotBlocked is the unit. MissingClauses is dominant. StuckOn{} should be propagated, if tied, we take the left.

Defined in Agda.Syntax.Internal.Blockers

Methods

(<>) :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t

sconcat :: NonEmpty (NotBlocked' t) -> NotBlocked' t

stimes :: Integral b => b -> NotBlocked' t -> NotBlocked' t

Semigroup a => Semigroup (Range' a)

Defined in Agda.Syntax.Position

Methods

(<>) :: Range' a -> Range' a -> Range' a

sconcat :: NonEmpty (Range' a) -> Range' a

stimes :: Integral b => b -> Range' a -> Range' a

Semigroup (CallGraph cinfo)

CallGraph is a monoid under union.

Defined in Agda.Termination.CallGraph

Methods

(<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo

sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo

stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo

Semigroup (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

(<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo

stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo

Semigroup m => Semigroup (TerM m)

Defined in Agda.Termination.Monad

Methods

(<>) :: TerM m -> TerM m -> TerM m

sconcat :: NonEmpty (TerM m) -> TerM m

stimes :: Integral b => b -> TerM m -> TerM m

Semigroup m => Semigroup (Case m)

Defined in Agda.TypeChecking.CompiledClause

Methods

(<>) :: Case m -> Case m -> Case m

sconcat :: NonEmpty (Case m) -> Case m

stimes :: Integral b => b -> Case m -> Case m

Semigroup c => Semigroup (WithArity c)

Defined in Agda.TypeChecking.CompiledClause

Methods

(<>) :: WithArity c -> WithArity c -> WithArity c

sconcat :: NonEmpty (WithArity c) -> WithArity c

stimes :: Integral b => b -> WithArity c -> WithArity c

Semigroup a => Semigroup (VarMap' a)

Proper monoid instance for VarMap rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using mappend.

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: VarMap' a -> VarMap' a -> VarMap' a

sconcat :: NonEmpty (VarMap' a) -> VarMap' a

stimes :: Integral b => b -> VarMap' a -> VarMap' a

Semigroup a => Semigroup (VarOcc' a)

The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair (t₁,t₂) then and t₁ has o₁ the occurrences of a variable x and t₂ has o₂ the occurrences of the same variable, then (t₁,t₂) has mappend o₁ o₂ occurrences of that variable.

From counting Quantity, we extrapolate this to FlexRig and Relevance: we care most about about StronglyRigid Relevant occurrences. E.g., if t₁ has a StronglyRigid occurrence and t₂ a Flexible occurrence, then (t₁,t₂) still has a StronglyRigid occurrence. Analogously, Relevant occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant.

VarOcc' forms a semiring, and this monoid is the addition of the semiring.

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: VarOcc' a -> VarOcc' a -> VarOcc' a

sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a

stimes :: Integral b => b -> VarOcc' a -> VarOcc' a

Semigroup (TCM Doc)

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Defined in Agda.TypeChecking.Pretty

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

Semigroup (Match a)

Defined in Agda.TypeChecking.Patterns.Match

Methods

(<>) :: Match a -> Match a -> Match a

sconcat :: NonEmpty (Match a) -> Match a

stimes :: Integral b => b -> Match a -> Match a

Ord a => Semigroup (Bag a)

Defined in Agda.Utils.Bag

Methods

(<>) :: Bag a -> Bag a -> Bag a

sconcat :: NonEmpty (Bag a) -> Bag a

stimes :: Integral b => b -> Bag a -> Bag a

PartialOrd a => Semigroup (Favorites a)

Favorites forms a Monoid under empty and 'union.

Defined in Agda.Utils.Favorites

Methods

(<>) :: Favorites a -> Favorites a -> Favorites a

sconcat :: NonEmpty (Favorites a) -> Favorites a

stimes :: Integral b => b -> Favorites a -> Favorites a

Semigroup a => Semigroup (RangeMap a)

Merges RangeMaps by inserting every "piece" of the smaller one into the larger one.

Defined in Agda.Utils.RangeMap

Methods

(<>) :: RangeMap a -> RangeMap a -> RangeMap a

sconcat :: NonEmpty (RangeMap a) -> RangeMap a

stimes :: Integral b => b -> RangeMap a -> RangeMap a

Bits a => Semigroup (And a)

Since: base-4.16

Defined in Data.Bits

Methods

(<>) :: And a -> And a -> And a

sconcat :: NonEmpty (And a) -> And a

stimes :: Integral b => b -> And a -> And a

FiniteBits a => Semigroup (Iff a)

This constraint is arguably too strong. However, as some types (such as Natural) have undefined complement, this is the only safe choice.

Since: base-4.16

Defined in Data.Bits

Methods

(<>) :: Iff a -> Iff a -> Iff a

sconcat :: NonEmpty (Iff a) -> Iff a

stimes :: Integral b => b -> Iff a -> Iff a

Bits a => Semigroup (Ior a)

Since: base-4.16

Defined in Data.Bits

Methods

(<>) :: Ior a -> Ior a -> Ior a

sconcat :: NonEmpty (Ior a) -> Ior a

stimes :: Integral b => b -> Ior a -> Ior a

Bits a => Semigroup (Xor a)

Since: base-4.16

Defined in Data.Bits

Methods

(<>) :: Xor a -> Xor a -> Xor a

sconcat :: NonEmpty (Xor a) -> Xor a

stimes :: Integral b => b -> Xor a -> Xor a

Semigroup a => Semigroup (Identity a)

Since: base-4.9.0.0

Defined in Data.Functor.Identity

Methods

(<>) :: Identity a -> Identity a -> Identity a

sconcat :: NonEmpty (Identity a) -> Identity a

stimes :: Integral b => b -> Identity a -> Identity a

Ord a => Semigroup (Max a)

Since: base-4.11.0.0

Defined in Data.Functor.Utils

Methods

(<>) :: Max a -> Max a -> Max a

sconcat :: NonEmpty (Max a) -> Max a

stimes :: Integral b => b -> Max a -> Max a

Ord a => Semigroup (Min a)

Since: base-4.11.0.0

Defined in Data.Functor.Utils

Methods

(<>) :: Min a -> Min a -> Min a

sconcat :: NonEmpty (Min a) -> Min a

stimes :: Integral b => b -> Min a -> Min a

Semigroup (First a)

Since: base-4.9.0.0

Defined in Data.Monoid

Methods

(<>) :: First a -> First a -> First a

sconcat :: NonEmpty (First a) -> First a

stimes :: Integral b => b -> First a -> First a

Semigroup (Last a)

Since: base-4.9.0.0

Defined in Data.Monoid

Methods

(<>) :: Last a -> Last a -> Last a

sconcat :: NonEmpty (Last a) -> Last a

stimes :: Integral b => b -> Last a -> Last a

Semigroup a => Semigroup (Down a)

Since: base-4.11.0.0

Defined in Data.Ord

Methods

(<>) :: Down a -> Down a -> Down a

sconcat :: NonEmpty (Down a) -> Down a

stimes :: Integral b => b -> Down a -> Down a

Semigroup (First a)

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

(<>) :: First a -> First a -> First a

sconcat :: NonEmpty (First a) -> First a

stimes :: Integral b => b -> First a -> First a

Semigroup (Last a)

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

(<>) :: Last a -> Last a -> Last a

sconcat :: NonEmpty (Last a) -> Last a

stimes :: Integral b => b -> Last a -> Last a

Ord a => Semigroup (Max a)

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

(<>) :: Max a -> Max a -> Max a

sconcat :: NonEmpty (Max a) -> Max a

stimes :: Integral b => b -> Max a -> Max a

Ord a => Semigroup (Min a)

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

(<>) :: Min a -> Min a -> Min a

sconcat :: NonEmpty (Min a) -> Min a

stimes :: Integral b => b -> Min a -> Min a

Monoid m => Semigroup (WrappedMonoid m)

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

(<>) :: WrappedMonoid m -> WrappedMonoid m -> WrappedMonoid m

sconcat :: NonEmpty (WrappedMonoid m) -> WrappedMonoid m

stimes :: Integral b => b -> WrappedMonoid m -> WrappedMonoid m

Semigroup a => Semigroup (Dual a)

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Dual a -> Dual a -> Dual a

sconcat :: NonEmpty (Dual a) -> Dual a

stimes :: Integral b => b -> Dual a -> Dual a

Semigroup (Endo a)

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Endo a -> Endo a -> Endo a

sconcat :: NonEmpty (Endo a) -> Endo a

stimes :: Integral b => b -> Endo a -> Endo a

Num a => Semigroup (Product a)

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Product a -> Product a -> Product a

sconcat :: NonEmpty (Product a) -> Product a

stimes :: Integral b => b -> Product a -> Product a

Num a => Semigroup (Sum a)

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Sum a -> Sum a -> Sum a

sconcat :: NonEmpty (Sum a) -> Sum a

stimes :: Integral b => b -> Sum a -> Sum a

Semigroup p => Semigroup (Par1 p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: Par1 p -> Par1 p -> Par1 p

sconcat :: NonEmpty (Par1 p) -> Par1 p

stimes :: Integral b => b -> Par1 p -> Par1 p

Semigroup (PutM ())

Defined in Data.Binary.Put

Methods

(<>) :: PutM () -> PutM () -> PutM ()

sconcat :: NonEmpty (PutM ()) -> PutM ()

stimes :: Integral b => b -> PutM () -> PutM ()

Monoid a => Semigroup (MarkupM a)

Defined in Text.Blaze.Internal

Methods

(<>) :: MarkupM a -> MarkupM a -> MarkupM a

sconcat :: NonEmpty (MarkupM a) -> MarkupM a

stimes :: Integral b => b -> MarkupM a -> MarkupM a

Semigroup (IntMap a)

Since: containers-0.5.7

Defined in Data.IntMap.Internal

Methods

(<>) :: IntMap a -> IntMap a -> IntMap a

sconcat :: NonEmpty (IntMap a) -> IntMap a

stimes :: Integral b => b -> IntMap a -> IntMap a

Semigroup (Seq a)

Since: containers-0.5.7

Defined in Data.Sequence.Internal

Methods

(<>) :: Seq a -> Seq a -> Seq a

sconcat :: NonEmpty (Seq a) -> Seq a

stimes :: Integral b => b -> Seq a -> Seq a

Semigroup (MergeSet a)

Defined in Data.Set.Internal

Methods

(<>) :: MergeSet a -> MergeSet a -> MergeSet a

sconcat :: NonEmpty (MergeSet a) -> MergeSet a

stimes :: Integral b => b -> MergeSet a -> MergeSet a

Ord a => Semigroup (Set a)

Since: containers-0.5.7

Defined in Data.Set.Internal

Methods

(<>) :: Set a -> Set a -> Set a

sconcat :: NonEmpty (Set a) -> Set a

stimes :: Integral b => b -> Set a -> Set a

Semigroup s => Semigroup (CI s)

Defined in Data.CaseInsensitive.Internal

Methods

(<>) :: CI s -> CI s -> CI s

sconcat :: NonEmpty (CI s) -> CI s

stimes :: Integral b => b -> CI s -> CI s

Semigroup (DNonEmpty a)

Defined in Data.DList.DNonEmpty.Internal

Methods

(<>) :: DNonEmpty a -> DNonEmpty a -> DNonEmpty a

sconcat :: NonEmpty (DNonEmpty a) -> DNonEmpty a

stimes :: Integral b => b -> DNonEmpty a -> DNonEmpty a

Semigroup (DList a)

Defined in Data.DList.Internal

Methods

(<>) :: DList a -> DList a -> DList a

sconcat :: NonEmpty (DList a) -> DList a

stimes :: Integral b => b -> DList a -> DList a

Semigroup a => Semigroup (IO a)

Since: base-4.10.0.0

Defined in GHC.Base

Methods

(<>) :: IO a -> IO a -> IO a

sconcat :: NonEmpty (IO a) -> IO a

stimes :: Integral b => b -> IO a -> IO a

(Hashable a, Eq a) => Semigroup (HashSet a)

Defined in Data.HashSet.Internal

Methods

(<>) :: HashSet a -> HashSet a -> HashSet a

sconcat :: NonEmpty (HashSet a) -> HashSet a

stimes :: Integral b => b -> HashSet a -> HashSet a

Semigroup (Doc a)

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(<>) :: Doc a -> Doc a -> Doc a

sconcat :: NonEmpty (Doc a) -> Doc a

stimes :: Integral b => b -> Doc a -> Doc a

Semigroup (Array a)

Defined in Data.Primitive.Array

Methods

(<>) :: Array a -> Array a -> Array a

sconcat :: NonEmpty (Array a) -> Array a

stimes :: Integral b => b -> Array a -> Array a

Semigroup (PrimArray a)

Defined in Data.Primitive.PrimArray

Methods

(<>) :: PrimArray a -> PrimArray a -> PrimArray a

sconcat :: NonEmpty (PrimArray a) -> PrimArray a

stimes :: Integral b => b -> PrimArray a -> PrimArray a

Semigroup (SmallArray a)

Defined in Data.Primitive.SmallArray

Methods

(<>) :: SmallArray a -> SmallArray a -> SmallArray a

sconcat :: NonEmpty (SmallArray a) -> SmallArray a

stimes :: Integral b => b -> SmallArray a -> SmallArray a

Semigroup (KeyMap v)

Defined in Data.Aeson.KeyMap

Methods

(<>) :: KeyMap v -> KeyMap v -> KeyMap v

sconcat :: NonEmpty (KeyMap v) -> KeyMap v

stimes :: Integral b => b -> KeyMap v -> KeyMap v

Semigroup (IResult a)

Defined in Data.Aeson.Types.Internal

Methods

(<>) :: IResult a -> IResult a -> IResult a

sconcat :: NonEmpty (IResult a) -> IResult a

stimes :: Integral b => b -> IResult a -> IResult a

Semigroup (Parser a)

Defined in Data.Aeson.Types.Internal

Methods

(<>) :: Parser a -> Parser a -> Parser a

sconcat :: NonEmpty (Parser a) -> Parser a

stimes :: Integral b => b -> Parser a -> Parser a

Semigroup (Result a)

Defined in Data.Aeson.Types.Internal

Methods

(<>) :: Result a -> Result a -> Result a

sconcat :: NonEmpty (Result a) -> Result a

stimes :: Integral b => b -> Result a -> Result a

Semigroup a => Semigroup (Maybe a)

Defined in Data.Strict.Maybe

Methods

(<>) :: Maybe a -> Maybe a -> Maybe a

sconcat :: NonEmpty (Maybe a) -> Maybe a

stimes :: Integral b => b -> Maybe a -> Maybe a

Semigroup a => Semigroup (Concurrently a)

Defined in Control.Concurrent.Async

Methods

(<>) :: Concurrently a -> Concurrently a -> Concurrently a

sconcat :: NonEmpty (Concurrently a) -> Concurrently a

stimes :: Integral b => b -> Concurrently a -> Concurrently a

Semigroup a => Semigroup (Q a)

Since: template-haskell-2.17.0.0

Defined in Language.Haskell.TH.Syntax

Methods

(<>) :: Q a -> Q a -> Q a

sconcat :: NonEmpty (Q a) -> Q a

stimes :: Integral b => b -> Q a -> Q a

Semigroup (Vector a)

Defined in Data.Vector

Methods

(<>) :: Vector a -> Vector a -> Vector a

sconcat :: NonEmpty (Vector a) -> Vector a

stimes :: Integral b => b -> Vector a -> Vector a

Prim a => Semigroup (Vector a)

Defined in Data.Vector.Primitive

Methods

(<>) :: Vector a -> Vector a -> Vector a

sconcat :: NonEmpty (Vector a) -> Vector a

stimes :: Integral b => b -> Vector a -> Vector a

Storable a => Semigroup (Vector a)

Defined in Data.Vector.Storable

Methods

(<>) :: Vector a -> Vector a -> Vector a

sconcat :: NonEmpty (Vector a) -> Vector a

stimes :: Integral b => b -> Vector a -> Vector a

Semigroup (NonEmpty a)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: NonEmpty a -> NonEmpty a -> NonEmpty a

sconcat :: NonEmpty (NonEmpty a) -> NonEmpty a

stimes :: Integral b => b -> NonEmpty a -> NonEmpty a

Semigroup a => Semigroup (Maybe a)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: Maybe a -> Maybe a -> Maybe a

sconcat :: NonEmpty (Maybe a) -> Maybe a

stimes :: Integral b => b -> Maybe a -> Maybe a

Semigroup a => Semigroup (a)

Since: base-4.15

Defined in GHC.Base

Methods

(<>) :: (a) -> (a) -> (a)

sconcat :: NonEmpty (a) -> (a)

stimes :: Integral b => b -> (a) -> (a)

Semigroup [a]

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: [a] -> [a] -> [a]

sconcat :: NonEmpty [a] -> [a]

stimes :: Integral b => b -> [a] -> [a]

(HasRange n, HasRange m) => Semigroup (ImportDirective' n m)

Defined in Agda.Syntax.Common

Methods

(<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m

sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m

stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m

Semigroup (Using' n m)

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' n m -> Using' n m -> Using' n m

sconcat :: NonEmpty (Using' n m) -> Using' n m

stimes :: Integral b => b -> Using' n m -> Using' n m

Semigroup a => Semigroup (Blocked' t a)

Defined in Agda.Syntax.Internal.Blockers

Methods

(<>) :: Blocked' t a -> Blocked' t a -> Blocked' t a

sconcat :: NonEmpty (Blocked' t a) -> Blocked' t a

stimes :: Integral b => b -> Blocked' t a -> Blocked' t a

(Monad m, Semigroup a) => Semigroup (PureConversionT m a)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

(<>) :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a

sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a

stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a

(MonadIO m, Semigroup a) => Semigroup (TCMT m a)

Strict (non-shortcut) semigroup.

Note that there might be a lazy alternative, e.g., for TCM All we might want and2M as concatenation, to shortcut conjunction in case we already have False.

Defined in Agda.TypeChecking.Monad.Base

Methods

(<>) :: TCMT m a -> TCMT m a -> TCMT m a

sconcat :: NonEmpty (TCMT m a) -> TCMT m a

stimes :: Integral b => b -> TCMT m a -> TCMT m a

Monad m => Semigroup (ListT m a)

Defined in Agda.Utils.ListT

Methods

(<>) :: ListT m a -> ListT m a -> ListT m a

sconcat :: NonEmpty (ListT m a) -> ListT m a

stimes :: Integral b => b -> ListT m a -> ListT m a

Semigroup (Either a b)

Since: base-4.9.0.0

Defined in Data.Either

Methods

(<>) :: Either a b -> Either a b -> Either a b

sconcat :: NonEmpty (Either a b) -> Either a b

stimes :: Integral b0 => b0 -> Either a b -> Either a b

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Semigroup (U1 p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: U1 p -> U1 p -> U1 p

sconcat :: NonEmpty (U1 p) -> U1 p

stimes :: Integral b => b -> U1 p -> U1 p

Semigroup (V1 p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: V1 p -> V1 p -> V1 p

sconcat :: NonEmpty (V1 p) -> V1 p

stimes :: Integral b => b -> V1 p -> V1 p

Semigroup a => Semigroup (ST s a)

Since: base-4.11.0.0

Defined in GHC.ST

Methods

(<>) :: ST s a -> ST s a -> ST s a

sconcat :: NonEmpty (ST s a) -> ST s a

stimes :: Integral b => b -> ST s a -> ST s a

Ord k => Semigroup (Map k v)

Defined in Data.Map.Internal

Methods

(<>) :: Map k v -> Map k v -> Map k v

sconcat :: NonEmpty (Map k v) -> Map k v

stimes :: Integral b => b -> Map k v -> Map k v

(Eq k, Hashable k) => Semigroup (HashMap k v)

Defined in Data.HashMap.Internal

Methods

(<>) :: HashMap k v -> HashMap k v -> HashMap k v

sconcat :: NonEmpty (HashMap k v) -> HashMap k v

stimes :: Integral b => b -> HashMap k v -> HashMap k v

Semigroup (Either a b)

Defined in Data.Strict.Either

Methods

(<>) :: Either a b -> Either a b -> Either a b

sconcat :: NonEmpty (Either a b) -> Either a b

stimes :: Integral b0 => b0 -> Either a b -> Either a b

(Semigroup a, Semigroup b) => Semigroup (These a b)

Defined in Data.Strict.These

Methods

(<>) :: These a b -> These a b -> These a b

sconcat :: NonEmpty (These a b) -> These a b

stimes :: Integral b0 => b0 -> These a b -> These a b

(Semigroup a, Semigroup b) => Semigroup (Pair a b)

Defined in Data.Strict.Tuple

Methods

(<>) :: Pair a b -> Pair a b -> Pair a b

sconcat :: NonEmpty (Pair a b) -> Pair a b

stimes :: Integral b0 => b0 -> Pair a b -> Pair a b

(Semigroup a, Semigroup b) => Semigroup (These a b)

Defined in Data.These

Methods

(<>) :: These a b -> These a b -> These a b

sconcat :: NonEmpty (These a b) -> These a b

stimes :: Integral b0 => b0 -> These a b -> These a b

Semigroup (Parser i a)

Defined in Data.Attoparsec.Internal.Types

Methods

(<>) :: Parser i a -> Parser i a -> Parser i a

sconcat :: NonEmpty (Parser i a) -> Parser i a

stimes :: Integral b => b -> Parser i a -> Parser i a

Semigroup b => Semigroup (a -> b)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: (a -> b) -> (a -> b) -> a -> b

sconcat :: NonEmpty (a -> b) -> a -> b

stimes :: Integral b0 => b0 -> (a -> b) -> a -> b

(Semigroup a, Semigroup b) => Semigroup (a, b)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: (a, b) -> (a, b) -> (a, b)

sconcat :: NonEmpty (a, b) -> (a, b)

stimes :: Integral b0 => b0 -> (a, b) -> (a, b)

Semigroup a => Semigroup (Const a b)

Since: base-4.9.0.0

Defined in Data.Functor.Const

Methods

(<>) :: Const a b -> Const a b -> Const a b

sconcat :: NonEmpty (Const a b) -> Const a b

stimes :: Integral b0 => b0 -> Const a b -> Const a b

(Applicative f, Semigroup a) => Semigroup (Ap f a)

Since: base-4.12.0.0

Defined in Data.Monoid

Methods

(<>) :: Ap f a -> Ap f a -> Ap f a

sconcat :: NonEmpty (Ap f a) -> Ap f a

stimes :: Integral b => b -> Ap f a -> Ap f a

Alternative f => Semigroup (Alt f a)

Since: base-4.9.0.0

Defined in Data.Semigroup.Internal

Methods

(<>) :: Alt f a -> Alt f a -> Alt f a

sconcat :: NonEmpty (Alt f a) -> Alt f a

stimes :: Integral b => b -> Alt f a -> Alt f a

Semigroup (f p) => Semigroup (Rec1 f p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: Rec1 f p -> Rec1 f p -> Rec1 f p

sconcat :: NonEmpty (Rec1 f p) -> Rec1 f p

stimes :: Integral b => b -> Rec1 f p -> Rec1 f p

Semigroup a => Semigroup (Tagged s a)

Defined in Data.Tagged

Methods

(<>) :: Tagged s a -> Tagged s a -> Tagged s a

sconcat :: NonEmpty (Tagged s a) -> Tagged s a

stimes :: Integral b => b -> Tagged s a -> Tagged s a

(Applicative m, Semigroup doc) => Semigroup (ReaderT s m doc)

Defined in Agda.Utils.Semigroup

Methods

(<>) :: ReaderT s m doc -> ReaderT s m doc -> ReaderT s m doc

sconcat :: NonEmpty (ReaderT s m doc) -> ReaderT s m doc

stimes :: Integral b => b -> ReaderT s m doc -> ReaderT s m doc

(Monad m, Semigroup doc) => Semigroup (StateT s m doc)

Defined in Agda.Utils.Semigroup

Methods

(<>) :: StateT s m doc -> StateT s m doc -> StateT s m doc

sconcat :: NonEmpty (StateT s m doc) -> StateT s m doc

stimes :: Integral b => b -> StateT s m doc -> StateT s m doc

Semigroup a => Semigroup (Constant a b)

Defined in Data.Functor.Constant

Methods

(<>) :: Constant a b -> Constant a b -> Constant a b

sconcat :: NonEmpty (Constant a b) -> Constant a b

stimes :: Integral b0 => b0 -> Constant a b -> Constant a b

(Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: (a, b, c) -> (a, b, c) -> (a, b, c)

sconcat :: NonEmpty (a, b, c) -> (a, b, c)

stimes :: Integral b0 => b0 -> (a, b, c) -> (a, b, c)

(Semigroup (f a), Semigroup (g a)) => Semigroup (Product f g a)

Since: base-4.16.0.0

Defined in Data.Functor.Product

Methods

(<>) :: Product f g a -> Product f g a -> Product f g a

sconcat :: NonEmpty (Product f g a) -> Product f g a

stimes :: Integral b => b -> Product f g a -> Product f g a

(Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p

sconcat :: NonEmpty ((f :*: g) p) -> (f :*: g) p

stimes :: Integral b => b -> (f :*: g) p -> (f :*: g) p

Semigroup c => Semigroup (K1 i c p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: K1 i c p -> K1 i c p -> K1 i c p

sconcat :: NonEmpty (K1 i c p) -> K1 i c p

stimes :: Integral b => b -> K1 i c p -> K1 i c p

(Semigroup a, Semigroup b, Semigroup c, Semigroup d) => Semigroup (a, b, c, d)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

sconcat :: NonEmpty (a, b, c, d) -> (a, b, c, d)

stimes :: Integral b0 => b0 -> (a, b, c, d) -> (a, b, c, d)

Semigroup (f (g a)) => Semigroup (Compose f g a)

Since: base-4.16.0.0

Defined in Data.Functor.Compose

Methods

(<>) :: Compose f g a -> Compose f g a -> Compose f g a

sconcat :: NonEmpty (Compose f g a) -> Compose f g a

stimes :: Integral b => b -> Compose f g a -> Compose f g a

Semigroup (f (g p)) => Semigroup ((f :.: g) p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: (f :.: g) p -> (f :.: g) p -> (f :.: g) p

sconcat :: NonEmpty ((f :.: g) p) -> (f :.: g) p

stimes :: Integral b => b -> (f :.: g) p -> (f :.: g) p

Semigroup (f p) => Semigroup (M1 i c f p)

Since: base-4.12.0.0

Defined in GHC.Generics

Methods

(<>) :: M1 i c f p -> M1 i c f p -> M1 i c f p

sconcat :: NonEmpty (M1 i c f p) -> M1 i c f p

stimes :: Integral b => b -> M1 i c f p -> M1 i c f p

(Semigroup a, Semigroup b, Semigroup c, Semigroup d, Semigroup e) => Semigroup (a, b, c, d, e)

Since: base-4.9.0.0

Defined in GHC.Base

Methods

(<>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

sconcat :: NonEmpty (a, b, c, d, e) -> (a, b, c, d, e)

stimes :: Integral b0 => b0 -> (a, b, c, d, e) -> (a, b, c, d, e)

type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m)

We need: - Read access to the AbsToCon environment - Read access to the TC environment - Read access to the TC state - Read and write access to the stConcreteNames part of the TC state - Read access to the options - Permission to print debug messages

Orphan instances

Semigroup (TCM Doc)

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc