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 Bool

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Range

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Permutation

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM MetaId

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ArgName

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Relevance

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Quantity

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Quantity -> 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 QName

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Polarity

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ProblemId

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Comparison

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM TCWarning

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

PrettyTCM TCErr

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM Warning

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

PrettyTCM ModuleName

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM QName

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Literal

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Occurrence

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM SplitTag

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM EqualityView

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM DBPatVar

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Clause

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Clause -> 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 Type

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Elim

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ConHead

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ConHead -> 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 Expr

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Expr -> 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 NegativeUnification

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM SplitError

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM CallInfo

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

PrettyTCM Call

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

PrettyTCM IsForced

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM RewriteRule

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => RewriteRule -> 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 DisplayTerm

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM TypeCheckingProblem

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM CompareAs

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Constraint

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ProblemConstraint

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM CheckpointId

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM PrettyContext

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NamedClause

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ElimType

Defined in Agda.TypeChecking.Records

Methods

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

PrettyTCM LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM Node

Defined in Agda.TypeChecking.Positivity

Methods

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

PrettyTCM SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

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

For debugging only.

Defined in Agda.TypeChecking.Coverage

Methods

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

PrettyTCM a => PrettyTCM [a]

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Seq OccursWhere)

Defined in Agda.TypeChecking.Positivity

Methods

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

Defined in Agda.TypeChecking.Pretty

Methods

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (WithHiding a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (QNamed Clause)

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Pattern' a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Elim' NLPat)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Elim' DisplayTerm)

Defined in Agda.TypeChecking.Pretty

Methods

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (MaybeReduced a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Judgement a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Closure a)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (LHSState a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LHSState a -> 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 b) => PrettyTCM (a, b)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => (a, b) -> 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 n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere))

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => WithNode n (Edge OccursWhere) -> 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_ :: (Monad m, Semigroup (m Doc)) => [m Doc] -> m Doc

prettyList without the brackets.

pretty :: (Monad 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 :: Monad m => [m Doc] -> m Doc

fsep :: Monad m => [m Doc] -> m Doc

hsep :: Monad m => [m Doc] -> m Doc

vcat :: Monad m => [m Doc] -> m Doc

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

data WithNode n a

Pairing something with a node (for printing only).

Constructors

WithNode n a

Instances

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere))

Defined in Agda.TypeChecking.Positivity

Methods

prettyTCM :: MonadPretty m => WithNode n (Edge OccursWhere) -> m Doc

type Doc = Doc

comma :: Monad m => m Doc

colon :: Monad m => m Doc

equals :: Monad m => m Doc

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

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

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

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

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

hcat :: Monad m => [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

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

prettyList :: (Monad m, Semigroup (m Doc)) => [m Doc] -> m Doc

Comma-separated list in brackets.

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

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

Pretty print with a given context precedence

prettyR :: (ToAbstract r a, PrettyTCM a, 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 associativity law:

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

Since: base-4.9.0.0

Methods

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

An associative operation.

Instances

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

Since: base-4.9.0.0

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty () -> ()

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

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 Builder

Defined in Data.ByteString.Builder.Internal

Methods

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

sconcat :: NonEmpty Builder -> Builder

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

Semigroup Series

Defined in Data.Aeson.Encoding.Internal

Methods

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

sconcat :: NonEmpty Series -> Series

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

Semigroup More

Defined in Data.Attoparsec.Internal.Types

Methods

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

sconcat :: NonEmpty More -> More

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

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

Defined in Data.ByteString.Short.Internal

Methods

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

sconcat :: NonEmpty ShortByteString -> ShortByteString

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

Semigroup AttributeValue

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty AttributeValue -> AttributeValue

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

Semigroup Attribute

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty Attribute -> Attribute

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

Semigroup ChoiceString

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty ChoiceString -> ChoiceString

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

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

Additive

Defined in Data.Time.LocalTime.Compat

Methods

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

sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime

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

Semigroup CalendarDiffDays

Additive

Defined in Data.Time.Calendar.Compat

Methods

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

sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays

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

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 CoverageCheck

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty CoverageCheck -> CoverageCheck

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

Semigroup PositivityCheck

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty PositivityCheck -> PositivityCheck

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

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 FreeVariables

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty FreeVariables -> FreeVariables

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

Semigroup Cohesion

Cohesion forms a semigroup under composition.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Cohesion -> Cohesion

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

Semigroup Relevance

Relevance forms a semigroup under composition.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Relevance -> Relevance

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

Semigroup Quantity

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Quantity -> Quantity

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

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

Pointwise composition.

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Modality -> Modality

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

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

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty CompressedFile -> CompressedFile

stimes :: Integral b => b -> CompressedFile -> CompressedFile

Semigroup File

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty File -> File

stimes :: Integral b => b -> File -> File

Semigroup TokenBased

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty TokenBased -> TokenBased

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

Semigroup Aspects

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty Aspects -> Aspects

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

Semigroup Blocked_

Defined in Agda.Syntax.Internal

Methods

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

sconcat :: NonEmpty Blocked_ -> Blocked_

stimes :: Integral b => b -> Blocked_ -> Blocked_

Semigroup NotBlocked

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

Defined in Agda.Syntax.Internal

Methods

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

sconcat :: NonEmpty NotBlocked -> NotBlocked

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

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 VarCounts

Defined in Agda.TypeChecking.Free

Methods

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

sconcat :: NonEmpty VarCounts -> VarCounts

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

Semigroup Simplification

Defined in Agda.TypeChecking.Monad.Base

Methods

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

sconcat :: NonEmpty Simplification -> Simplification

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

Semigroup Slot

Defined in Data.HashTable.ST.Basic

Methods

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

sconcat :: NonEmpty Slot -> Slot

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

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 LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns

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

Semigroup FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

sconcat :: NonEmpty FlexChoice -> FlexChoice

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

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 CallPath

Defined in Agda.Termination.Monad

Methods

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

sconcat :: NonEmpty CallPath -> CallPath

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

Semigroup ClausesPostChecks

Defined in Agda.TypeChecking.Rules.Def

Methods

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

sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks

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

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 [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]

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 (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 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 (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 (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 (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 a => Semigroup (Concurrently a)

Only defined by async for base >= 4.9

Since: async-2.1.0

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

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

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

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

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

Since: base-4.9.0.0

Defined in Data.Semigroup

Methods

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

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

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

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

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

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

Defined in Data.DList

Methods

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

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

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

Since: primitive-0.6.4.0

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)

Since: primitive-0.6.3.0

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

Since: primitive-0.6.3.0

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 a => Semigroup (Maybe a)

Defined in Agda.Utils.Maybe.Strict

Methods

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

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

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

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

Defined in Data.HashSet.Base

Methods

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

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

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

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

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

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

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

Semigroup (TCM Doc)

Defined in Agda.TypeChecking.Warnings

Methods

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

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

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

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

Semigroup a => Semigroup (OccM a)

Defined in Agda.TypeChecking.Positivity

Methods

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

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

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

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

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

Defined in Data.HashMap.Base

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

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

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

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

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

Monad m => Semigroup (StateT s m Doc)

Defined in Agda.TypeChecking.Warnings

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

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

Applicative m => Semigroup (ReaderT s m Doc)

Defined in Agda.TypeChecking.Warnings

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

(Applicative m, Semigroup c) => Semigroup (FreeT a b m c)

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c

sconcat :: NonEmpty (FreeT a b m c) -> FreeT a b m c

stimes :: Integral b0 => b0 -> FreeT a b m c -> FreeT a b m c

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