Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Pretty

Synopsis

Documentation

newtype PrettyContext Source #

Constructors

PrettyContext Context 

Instances

Instances details
PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

class PrettyTCM a where Source #

Methods

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

Instances

Instances details
PrettyTCM Bool Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ArgName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Modality Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Nat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM Warning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Literal Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM NegativeUnification Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

PrettyTCM Call Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

PrettyTCM IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM NamedClause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ElimType Source # 
Instance details

Defined in Agda.TypeChecking.Records

PrettyTCM LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

PrettyTCM SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

PrettyTCM HypSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM SizeConstraint Source #

Assumes we are in the right context.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

PrettyTCM SplitClause Source #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

PrettyTCM a => PrettyTCM [a] Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM a => PrettyTCM (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (MaybeReduced a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM a => PrettyTCM (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM a => PrettyTCM (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (LHSState a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM a => PrettyTCM (Masked a) Source #

Print masked things in double parentheses.

Instance details

Defined in Agda.Termination.Monad

Methods

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

(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

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

prettyList_ :: (Monad m, Semigroup (m Doc)) => [m Doc] -> m Doc Source #

prettyList without the brackets.

pretty :: (Monad m, Pretty a) => a -> m Doc Source #

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

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

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

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

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

sep :: Monad m => [m Doc] -> m Doc Source #

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

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

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

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

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a 

Instances

Instances details
PrettyTCM n => PrettyTCM (WithNode n Occurrence) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

type Doc = Doc Source #

comma :: Monad m => m Doc Source #

colon :: Monad m => m Doc Source #

equals :: Monad m => m Doc Source #

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

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

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

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

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

hcat :: Monad m => [m Doc] -> m Doc Source #

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

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

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

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

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

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

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

Comma-separated list in brackets.

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

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

Pretty print with a given context precedence

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

Proper pretty printing of patterns:

class Semigroup a where #

Methods

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

Instances

Instances details
Semigroup Ordering 
Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty Ordering -> Ordering

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

Semigroup () 
Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty () -> ()

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

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Internal

Methods

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

sconcat :: NonEmpty ByteString -> ByteString

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

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

Methods

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

sconcat :: NonEmpty ByteString -> ByteString

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

Semigroup Builder 
Instance details

Defined in Data.ByteString.Builder.Internal

Methods

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

sconcat :: NonEmpty Builder -> Builder

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

Semigroup Series 
Instance details

Defined in Data.Aeson.Encoding.Internal

Methods

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

sconcat :: NonEmpty Series -> Series

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

Semigroup AttributeValue 
Instance details

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty AttributeValue -> AttributeValue

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

Semigroup Attribute 
Instance details

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty Attribute -> Attribute

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

Semigroup Any 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty Any -> Any

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

Semigroup All 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty All -> All

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

Semigroup CalendarDiffDays 
Instance details

Defined in Data.Time.Calendar.CalendarDiffDays

Methods

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

sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays

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

Semigroup CalendarDiffTime 
Instance details

Defined in Data.Time.LocalTime.Internal.CalendarDiffTime

Methods

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

sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime

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

Semigroup IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

Methods

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

sconcat :: NonEmpty IntSet -> IntSet

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

Semigroup ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

Methods

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

sconcat :: NonEmpty ShortByteString -> ShortByteString

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

Semigroup Void 
Instance details

Defined in Data.Void

Methods

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

sconcat :: NonEmpty Void -> Void

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

Semigroup MaxNat Source # 
Instance details

Defined in Agda.Utils.Monoid

Methods

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

sconcat :: NonEmpty MaxNat -> MaxNat

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

Semigroup IntSet 
Instance details

Defined in Data.IntSet.Internal

Methods

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

sconcat :: NonEmpty IntSet -> IntSet

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

Semigroup Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

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

sconcat :: NonEmpty Doc -> Doc

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

Semigroup PartialOrdering Source #

Partial ordering forms a monoid under sequencing.

Instance details

Defined in Agda.Utils.PartialOrd

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty IsAbstract -> IsAbstract

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

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Cohesion Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Cohesion -> Cohesion

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

Semigroup Relevance Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Relevance -> Relevance

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

Semigroup Quantity Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Quantity -> Quantity

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

Semigroup QωOrigin Source #

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

Instance details

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

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

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Q1Origin -> Q1Origin

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

Semigroup Q0Origin Source #

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

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Q0Origin -> Q0Origin

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

Semigroup Modality Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Modality -> Modality

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

Semigroup Hiding Source #

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

Instance details

Defined in Agda.Syntax.Common

Methods

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

sconcat :: NonEmpty Hiding -> Hiding

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

Semigroup Overlappable Source #

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

Instance details

Defined in Agda.Syntax.Common

Semigroup CompressedFile Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup File Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty File -> File

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

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty TokenBased -> TokenBased

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

Semigroup Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Methods

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

sconcat :: NonEmpty Aspects -> Aspects

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

Semigroup Blocked_ Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

sconcat :: NonEmpty Blocked_ -> Blocked_

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

Semigroup NotBlocked Source #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

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

sconcat :: NonEmpty NotBlocked -> NotBlocked

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

Semigroup FlexRigMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

sconcat :: NonEmpty FlexRigMap -> FlexRigMap

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

Semigroup MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

sconcat :: NonEmpty MetaSet -> MetaSet

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

Semigroup VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

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

sconcat :: NonEmpty VarCounts -> VarCounts

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

Semigroup Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Semigroup ByteArray 
Instance details

Defined in Data.Primitive.ByteArray

Methods

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

sconcat :: NonEmpty ByteArray -> ByteArray

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

Semigroup Slot 
Instance details

Defined in Data.HashTable.ST.Basic

Methods

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

sconcat :: NonEmpty Slot -> Slot

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

Semigroup Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty Occurs -> Occurs

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

Semigroup SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty SeqArg -> SeqArg

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

Semigroup UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

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

sconcat :: NonEmpty UnderLambda -> UnderLambda

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

Semigroup LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

sconcat :: NonEmpty FlexChoice -> FlexChoice

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

Semigroup OccurrencesBuilder Source #

The semigroup laws only hold up to flattening of Concat.

Instance details

Defined in Agda.TypeChecking.Positivity

Semigroup CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

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

sconcat :: NonEmpty CallPath -> CallPath

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

Semigroup More 
Instance details

Defined in Data.Attoparsec.Internal.Types

Methods

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

sconcat :: NonEmpty More -> More

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

Semigroup ClausesPostChecks Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Def

Semigroup IsMain Source #

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Methods

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

sconcat :: NonEmpty IsMain -> IsMain

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

Semigroup ChoiceString 
Instance details

Defined in Text.Blaze.Internal

Methods

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

sconcat :: NonEmpty ChoiceString -> ChoiceString

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

Semigroup [a] 
Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (Maybe a) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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

Instance details

Defined in Control.Concurrent.Async

Methods

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

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

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

Semigroup a => Semigroup (Maybe a) Source # 
Instance details

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) 
Instance details

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

Semigroup (NonEmpty a) 
Instance details

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 (Identity a) 
Instance details

Defined in Data.Functor.Identity

Methods

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

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

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

Ord a => Semigroup (Set a) 
Instance details

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 a => Semigroup (Dual a) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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 a => Semigroup (Down a) 
Instance details

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) 
Instance details

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) 
Instance details

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 (PutM ()) 
Instance details

Defined in Data.Binary.Put

Methods

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

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

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

Semigroup (First a) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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

Semigroup a => Semigroup (Option a) 
Instance details

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

Monoid m => Semigroup (WrappedMonoid m) 
Instance details

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

Ord a => Semigroup (Bag a) Source # 
Instance details

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) 
Instance details

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 (IntMap a) 
Instance details

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) 
Instance details

Defined in Data.Sequence.Internal

Methods

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

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

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

Semigroup (Doc a) 
Instance details

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 (TCM Doc) Source # 
Instance details

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) Source #

Favorites forms a Monoid under empty and 'union.

Instance details

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) Source # 
Instance details

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) Source #

CallGraph is a monoid under union.

Instance details

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) Source #

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

Instance details

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) Source #

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.

Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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

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) 
Instance details

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) 
Instance details

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 (Vector a) 
Instance details

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) 
Instance details

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 (Match a) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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

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

Storable a => Semigroup (Vector a) 
Instance details

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

Monoid a => Semigroup (MarkupM a) 
Instance details

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 b => Semigroup (a -> b) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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)

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

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) 
Instance details

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 a => Semigroup (ST s a) 
Instance details

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

Semigroup (Proxy s) 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source #

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.

Instance details

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) Source # 
Instance details

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 (Parser i a) 
Instance details

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 (f p) => Semigroup (Rec1 f p) 
Instance details

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) 
Instance details

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) 
Instance details

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

Alternative f => Semigroup (Alt f a) 
Instance details

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

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

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

Applicative m => Semigroup (ReaderT s m Doc) Source # 
Instance details

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

Monad m => Semigroup (StateT s m Doc) Source # 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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 c) => Semigroup (FreeT a b m c) Source # 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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)