Agda.TypeChecking.Pretty

Documentation

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

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

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

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

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

colon :: Applicative m => m Doc

comma :: Applicative m => m Doc

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

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

type Doc = Doc

equals :: Applicative m => m Doc

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

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

hcat :: (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

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

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

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

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

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

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

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

prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> 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 Pattern

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern -> 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 Erased

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Erased -> 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 TopLevelModuleName

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

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

PrettyTCM SplitClause

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

prettyTCM :: MonadPretty m => SplitClause -> 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 ContextEntry

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ContextEntry -> 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 NamedMeta

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedMeta -> 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 NoLeftInv

Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Methods

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

PrettyTCM UnifyState

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Methods

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

PrettyTCM UnifyStep

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Methods

prettyTCM :: MonadPretty m => UnifyStep -> 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 Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

prettyTCM :: MonadPretty m => Flex -> 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 String)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg String -> 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 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

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

Defined in Agda.Interaction.BasicOps

Methods

prettyTCM :: MonadPretty m => OutputForm a b -> 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

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

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

prettyList without the brackets.

type MonadPretty (m :: Type -> Type) = MonadAbsToCon m

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.

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

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

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

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

newtype PrettyContext

Constructors

PrettyContext Context

Instances

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

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

prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> 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

data WithNode n a

Pairing something with a node (for printing only).

Constructors

WithNode n a

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

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

You can alternatively define sconcat instead of (<>), in which case the laws are:

Unit

sconcat (pure x) = x

Multiplication

sconcat (join xss) = sconcat (fmap sconcat xss)

Since: base-4.9.0.0

Minimal complete definition

(<>) | sconcat

Methods

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

An associative operation.

Examples

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

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

>>> putStr "Hello, " <> putStrLn "World!"
Hello, World!

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 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 PositionMap

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty PositionMap -> PositionMap

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

Semigroup OptionsPragma

Defined in Agda.Interaction.Library.Base

Methods

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

sconcat :: NonEmpty OptionsPragma -> OptionsPragma

stimes :: Integral b => b -> OptionsPragma -> OptionsPragma

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 JointOpacity

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty JointOpacity -> JointOpacity

stimes :: Integral b => b -> JointOpacity -> JointOpacity

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 Aspect

NameKind in Name can get more precise.

Defined in Agda.Syntax.Common.Aspect

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.Syntax.Common.Aspect

Methods

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

sconcat :: NonEmpty NameKind -> NameKind

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

Semigroup TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty TokenBased -> TokenBased

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

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 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 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 UnifyOutput

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Methods

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

sconcat :: NonEmpty UnifyOutput -> UnifyOutput

stimes :: Integral b => b -> UnifyOutput -> UnifyOutput

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 ByteArray

Since: base-4.17.0.0

Defined in Data.Array.Byte

Methods

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

sconcat :: NonEmpty ByteArray -> ByteArray

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

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 GHC.Base

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.Type

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 OsString

Defined in System.OsString.Internal.Types.Hidden

Methods

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

sconcat :: NonEmpty OsString -> OsString

stimes :: Integral b => b -> OsString -> OsString

Semigroup PosixString

Defined in System.OsString.Internal.Types.Hidden

Methods

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

sconcat :: NonEmpty PosixString -> PosixString

stimes :: Integral b => b -> PosixString -> PosixString

Semigroup WindowsString

Defined in System.OsString.Internal.Types.Hidden

Methods

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

sconcat :: NonEmpty WindowsString -> WindowsString

stimes :: Integral b => b -> WindowsString -> WindowsString

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 Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

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

sconcat :: NonEmpty Doc -> Doc

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

Semigroup SetTestInfo

Defined in Text.Regex.TDFA.CorePattern

Methods

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

sconcat :: NonEmpty SetTestInfo -> SetTestInfo

stimes :: Integral b => b -> SetTestInfo -> SetTestInfo

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 Builder

Defined in Data.Text.Internal.Builder

Methods

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

sconcat :: NonEmpty Builder -> Builder

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

Semigroup StrictBuilder

Concatenation of StrictBuilder is right-biased: the right builder will be run first. This allows a builder to run tail-recursively when it was accumulated left-to-right.

Defined in Data.Text.Internal.StrictBuilder

Methods

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

sconcat :: NonEmpty StrictBuilder -> StrictBuilder

stimes :: Integral b => b -> StrictBuilder -> StrictBuilder

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

Eq 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 (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

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

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

SmallSetElement a => Semigroup (SmallSet a)

Defined in Agda.Utils.SmallSet

Methods

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

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

stimes :: Integral b => b -> SmallSet a -> SmallSet 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 (FromMaybe b)

Defined in Data.Foldable1

Methods

(<>) :: FromMaybe b -> FromMaybe b -> FromMaybe b

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

stimes :: Integral b0 => b0 -> FromMaybe b -> FromMaybe b

Semigroup a => Semigroup (JoinWith a)

Defined in Data.Foldable1

Methods

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

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

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

Semigroup (NonEmptyDList a)

Defined in Data.Foldable1

Methods

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

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

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

Semigroup (Comparison a)

(<>) on comparisons combines results with (<>) @Ordering. Without newtypes this equals liftA2 (liftA2 (<>)).

(<>) :: Comparison a -> Comparison a -> Comparison a
Comparison cmp <> Comparison cmp' = Comparison a a' ->
  cmp a a' <> cmp a a'

Defined in Data.Functor.Contravariant

Methods

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

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

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

Semigroup (Equivalence a)

(<>) on equivalences uses logical conjunction (&&) on the results. Without newtypes this equals liftA2 (liftA2 (&&)).

(<>) :: Equivalence a -> Equivalence a -> Equivalence a
Equivalence equiv <> Equivalence equiv' = Equivalence a b ->
  equiv a b && equiv' a b

Defined in Data.Functor.Contravariant

Methods

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

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

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

Semigroup (Predicate a)

(<>) on predicates uses logical conjunction (&&) on the results. Without newtypes this equals liftA2 (&&).

(<>) :: Predicate a -> Predicate a -> Predicate a
Predicate pred <> Predicate pred' = Predicate a ->
  pred a && pred' a

Defined in Data.Functor.Contravariant

Methods

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

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

stimes :: Integral b => b -> Predicate a -> Predicate 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

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 (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 (STM a)

Since: base-4.17.0.0

Defined in GHC.Conc.Sync

Methods

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

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

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

(Generic a, Semigroup (Rep a ())) => Semigroup (Generically a)

Since: base-4.17.0.0

Defined in GHC.Generics

Methods

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

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

stimes :: Integral b => b -> Generically a -> Generically 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

Num a => Semigroup (AlphaColour a)

Defined in Data.Colour.Internal

Methods

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

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

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

Num a => Semigroup (Colour a)

Defined in Data.Colour.Internal

Methods

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

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

stimes :: Integral b => b -> Colour a -> Colour 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

Ord a => Semigroup (Intersection a)

Defined in Data.Set.Internal

Methods

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

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

stimes :: Integral b => b -> Intersection a -> Intersection 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

Semigroup (Validity k)

Defined in Data.HashMap.Internal.Debug

Methods

(<>) :: Validity k -> Validity k -> Validity k

sconcat :: NonEmpty (Validity k) -> Validity k

stimes :: Integral b => b -> Validity k -> Validity k

(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 (CharMap a)

Defined in Data.IntMap.CharMap2

Methods

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

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

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

Semigroup (EnumSet e)

Defined in Data.IntSet.EnumSet2

Methods

(<>) :: EnumSet e -> EnumSet e -> EnumSet e

sconcat :: NonEmpty (EnumSet e) -> EnumSet e

stimes :: Integral b => b -> EnumSet e -> EnumSet e

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.Internal

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 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 (Solo a)

Since: base-4.15

Defined in GHC.Base

Methods

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

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

stimes :: Integral b => b -> Solo a -> Solo 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 a => Semigroup (Op a b)

(<>) @(Op a b) without newtypes is (<>) @(b->a) = liftA2 (<>). This lifts the Semigroup operation (<>) over the output of a.

(<>) :: Op a b -> Op a b -> Op a b
Op f <> Op g = Op a -> f a <> g a

Defined in Data.Functor.Contravariant

Methods

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

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

stimes :: Integral b0 => b0 -> Op a b -> Op 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

Ord k => Semigroup (EnumMap k a)

Defined in Data.IntMap.EnumMap2

Methods

(<>) :: EnumMap k a -> EnumMap k a -> EnumMap k a

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

stimes :: Integral b => b -> EnumMap k a -> EnumMap k a

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 (ConcurrentlyE e a)

Defined in Control.Concurrent.Async.Internal

Methods

(<>) :: ConcurrentlyE e a -> ConcurrentlyE e a -> ConcurrentlyE e a

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

stimes :: Integral b => b -> ConcurrentlyE e a -> ConcurrentlyE e a

(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 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 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 :: Type -> Type) = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

The function runAbsToCon can target any monad that satisfies the constraints of MonadAbsToCon.

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