Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Pretty

Synopsis

newtype PrettyContext = PrettyContext Context
class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> 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
pretty :: (Monad m, Pretty a) => a -> m Doc
nest :: Functor m => Int -> m Doc -> m Doc
($$) :: Applicative m => m Doc -> m Doc -> m Doc
(<+>) :: Applicative m => m Doc -> m Doc -> m Doc
(<?>) :: Applicative m => m Doc -> m Doc -> m Doc
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 = WithNode n a
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
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
punctuate :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> [m Doc]
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
prettyR :: (ToAbstract r a, PrettyTCM a, MonadPretty m, MonadError TCErr m) => r -> m Doc
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
class Semigroup a where
- (<>) :: a -> a -> a

Documentation

newtype PrettyContext Source #

Constructors

PrettyContext Context

Instances

Instances details

PrettyTCM PrettyContext Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source #

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 Methods prettyTCM :: MonadPretty m => Permutation -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => Relevance -> m Doc Source #
PrettyTCM Quantity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Quantity -> m Doc Source #
PrettyTCM Modality Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Modality -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => Polarity -> m Doc Source #
PrettyTCM ProblemId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
PrettyTCM Comparison Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #
PrettyTCM TCWarning Source #
Instance details Defined in Agda.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => TCWarning -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => ModuleName -> 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 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 Methods prettyTCM :: MonadPretty m => Occurrence -> m Doc Source #
PrettyTCM SplitTag Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => SplitTag -> m Doc Source #
PrettyTCM EqualityView Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => EqualityView -> m Doc Source #
PrettyTCM DBPatVar Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DBPatVar -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
PrettyTCM TypedBinding Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
PrettyTCM UnificationFailure Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source #
PrettyTCM NegativeUnification Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source #
PrettyTCM SplitError Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source #
PrettyTCM CallInfo Source #
Instance details Defined in Agda.TypeChecking.Pretty.Call Methods prettyTCM :: MonadPretty m => CallInfo -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => IsForced -> m Doc Source #
PrettyTCM RewriteRule Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => RewriteRule -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => DisplayTerm -> m Doc Source #
PrettyTCM TypeCheckingProblem Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypeCheckingProblem -> m Doc Source #
PrettyTCM CompareAs Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CompareAs -> m Doc Source #
PrettyTCM Constraint Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Constraint -> m Doc Source #
PrettyTCM ProblemConstraint Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemConstraint -> m Doc Source #
PrettyTCM CheckpointId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CheckpointId -> m Doc Source #
PrettyTCM PrettyContext Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source #
PrettyTCM NamedClause Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
PrettyTCM ElimType Source #
Instance details Defined in Agda.TypeChecking.Records Methods prettyTCM :: MonadPretty m => ElimType -> m Doc Source #
PrettyTCM LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source #
PrettyTCM AbsurdPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source #
PrettyTCM DotPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => DotPattern -> m Doc Source #
PrettyTCM AsBinding Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AsBinding -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => SplitPatVar -> m Doc Source #
PrettyTCM HypSizeConstraint Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #
PrettyTCM SizeConstraint Source #	Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
PrettyTCM SizeMeta Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #
PrettyTCM ErrorPart Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods prettyTCM :: MonadPretty m => ErrorPart -> m Doc Source #
PrettyTCM SplitClause Source #	For debugging only.
Instance details Defined in Agda.TypeChecking.Coverage Methods prettyTCM :: MonadPretty m => SplitClause -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
(Pretty a, PrettyTCM a, Subst a a) => PrettyTCM (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #
PrettyTCM (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' NLPat -> m Doc Source #
PrettyTCM (Elim' DisplayTerm) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc Source #
(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 Methods prettyTCM :: MonadPretty m => MaybeReduced a -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => WithNode n Occurrence -> m Doc Source #
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => WithNode n (Edge OccursWhere) -> m Doc Source #
(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 Methods prettyTCM :: MonadPretty m => WithNode n Occurrence -> m Doc Source #
PrettyTCM n => PrettyTCM (WithNode n (Edge OccursWhere)) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCM :: MonadPretty m => WithNode n (Edge OccursWhere) -> m Doc Source #

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

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

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

Proper pretty printing of patterns:

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

class Semigroup a where #

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

Instances should satisfy the following:

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

Since: base-4.9.0.0

Methods

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

An associative operation.

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

Instances

Instances details

Semigroup Ordering	Since: base-4.9.0.0
Instance details 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
Instance details Defined in GHC.Base Methods (<>) :: () -> () -> () # sconcat :: NonEmpty () -> () # stimes :: Integral b => b -> () -> () #
Semigroup Void	Since: base-4.9.0.0
Instance details 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
Instance details 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
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Any -> Any -> Any # sconcat :: NonEmpty Any -> Any # stimes :: Integral b => b -> Any -> Any #
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 ByteString
Instance details Defined in Data.ByteString.Lazy.Internal Methods (<>) :: ByteString -> ByteString -> ByteString # sconcat :: NonEmpty ByteString -> ByteString # stimes :: Integral b => b -> ByteString -> ByteString #
Semigroup ByteString
Instance details Defined in Data.ByteString.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 IntSet	Since: containers-0.5.7
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 CalendarDiffTime	Additive
Instance details Defined in Data.Time.LocalTime.Internal.CalendarDiffTime Methods (<>) :: CalendarDiffTime -> CalendarDiffTime -> CalendarDiffTime # sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime # stimes :: Integral b => b -> CalendarDiffTime -> CalendarDiffTime #
Semigroup CalendarDiffDays	Additive
Instance details Defined in Data.Time.Calendar.CalendarDiffDays Methods (<>) :: CalendarDiffDays -> CalendarDiffDays -> CalendarDiffDays # sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays # stimes :: Integral b => b -> CalendarDiffDays -> CalendarDiffDays #
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 MaxNat Source #
Instance details Defined in Agda.Utils.Monoid Methods (<>) :: MaxNat -> MaxNat -> MaxNat # sconcat :: NonEmpty MaxNat -> MaxNat # stimes :: Integral b => b -> MaxNat -> MaxNat #
Semigroup PartialOrdering Source #	Partial ordering forms a monoid under sequencing.
Instance details Defined in Agda.Utils.PartialOrd Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering # sconcat :: NonEmpty PartialOrdering -> PartialOrdering # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering #
Semigroup CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck #
Semigroup PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck #
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 Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables # stimes :: Integral b => b -> FreeVariables -> FreeVariables #
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 Methods (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable # stimes :: Integral b => b -> Overlappable -> Overlappable #
Semigroup CompressedFile Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: CompressedFile -> CompressedFile -> CompressedFile # sconcat :: NonEmpty CompressedFile -> CompressedFile # stimes :: Integral b => b -> CompressedFile -> CompressedFile #
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 Methods (<>) :: Simplification -> Simplification -> Simplification # sconcat :: NonEmpty Simplification -> Simplification # stimes :: Integral b => b -> Simplification -> Simplification #
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 Methods (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns # stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns #
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 Methods (<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder # sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder # stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder #
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 Series
Instance details Defined in Data.Aeson.Encoding.Internal Methods (<>) :: Series -> Series -> Series # sconcat :: NonEmpty Series -> Series # stimes :: Integral b => b -> Series -> Series #
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 Methods (<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks # sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks # stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks #
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 Attribute
Instance details Defined in Text.Blaze.Internal Methods (<>) :: Attribute -> Attribute -> Attribute # sconcat :: NonEmpty Attribute -> Attribute # stimes :: Integral b => b -> Attribute -> Attribute #
Semigroup AttributeValue
Instance details Defined in Text.Blaze.Internal Methods (<>) :: AttributeValue -> AttributeValue -> AttributeValue # sconcat :: NonEmpty AttributeValue -> AttributeValue # stimes :: Integral b => b -> AttributeValue -> AttributeValue #
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]	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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)	Since: base-4.10.0.0
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)	Since: base-4.12.0.0
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 #
Ord a => Semigroup (Min a)	Since: base-4.9.0.0
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 #
Ord a => Semigroup (Max a)	Since: base-4.9.0.0
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 #
Semigroup (First a)	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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 #
Monoid m => Semigroup (WrappedMonoid m)	Since: base-4.9.0.0
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 #
Semigroup a => Semigroup (Option a)	Since: base-4.9.0.0
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 #
Semigroup a => Semigroup (Identity a)	Since: base-4.9.0.0
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 #
Semigroup (First a)	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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 a => Semigroup (Dual a)	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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 (Sum a)	Since: base-4.9.0.0
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 #
Num a => Semigroup (Product a)	Since: base-4.9.0.0
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 #
Semigroup a => Semigroup (Down a)	Since: base-4.11.0.0
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 (NonEmpty a)	Since: base-4.9.0.0
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 (PutM ())
Instance details Defined in Data.Binary.Put Methods (<>) :: PutM () -> PutM () -> PutM () # sconcat :: NonEmpty (PutM ()) -> PutM () # stimes :: Integral b => b -> PutM () -> PutM () #
Semigroup (IntMap a)	Since: containers-0.5.7
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)	Since: containers-0.5.7
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 #
Ord a => Semigroup (Set a)	Since: containers-0.5.7
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 (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 #
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 #
(Hashable a, Eq a) => Semigroup (HashSet a)
Instance details Defined in Data.HashSet.Internal Methods (<>) :: HashSet a -> HashSet a -> HashSet a # sconcat :: NonEmpty (HashSet a) -> HashSet a # stimes :: Integral b => b -> HashSet a -> HashSet a #
Semigroup 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 #
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 (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 (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 (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 (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 #
Semigroup a => Semigroup (Concurrently a)
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 #
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)	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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)	Since: base-4.12.0.0
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)	Since: base-4.12.0.0
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)	Since: base-4.9.0.0
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 a => Semigroup (ST s a)	Since: base-4.11.0.0
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)	Since: base-4.9.0.0
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 #
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 #
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 #
(Eq k, Hashable k) => Semigroup (HashMap k v)
Instance details Defined in Data.HashMap.Internal Methods (<>) :: HashMap k v -> HashMap k v -> HashMap k v # sconcat :: NonEmpty (HashMap k v) -> HashMap k v # stimes :: Integral b => b -> HashMap k v -> HashMap k v #
Semigroup (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)	Since: base-4.12.0.0
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)	Since: base-4.9.0.0
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)	Since: base-4.9.0.0
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 #
(Applicative f, Semigroup a) => Semigroup (Ap f a)	Since: base-4.12.0.0
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 #
Alternative f => Semigroup (Alt f a)	Since: base-4.9.0.0
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 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)	Since: base-4.12.0.0
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)	Since: base-4.12.0.0
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)	Since: base-4.9.0.0
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)	Since: base-4.12.0.0
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)	Since: base-4.12.0.0
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)	Since: base-4.9.0.0
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) #