Agda-2.6.2.0.20211129: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Expr -> 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 ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Blocker Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Literal Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM NamedClause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM SplitClause Source #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

PrettyTCM SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

PrettyTCM SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Call Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

PrettyTCM CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

PrettyTCM Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Constraint

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM IsForced 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 NegativeUnification Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Constraint

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ElimType Source # 
Instance details

Defined in Agda.TypeChecking.Records

PrettyTCM AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AnnotationPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

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

Defined in Agda.TypeChecking.Pretty

PrettyTCM String Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Bool Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Bool) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => WithHiding 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 (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom (Name, Type) -> 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 #

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

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Closure 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 (MaybeReduced a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (LHSState a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

prettyList without the brackets.

pretty :: (Applicative 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 :: (Applicative m, Foldable t) => t (m Doc) -> m Doc Source #

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

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

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

class PrettyTCMWithNode a where Source #

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

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a 

type Doc = Doc Source #

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

hcat :: (Applicative m, Foldable t) => t (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 #

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

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

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

Comma-separated list in brackets.

punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (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 #

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

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Semigroup Doc Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

sconcat :: NonEmpty Doc -> Doc #

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

Semigroup Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Semigroup UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Semigroup HsCompileState Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

Semigroup Occurs Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Semigroup SeqArg Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Semigroup UnderLambda Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Semigroup Aspect Source #

NameKind in Name can get more precise.

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup Aspects Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup NameKind Source #

Some NameKinds are more informative than others.

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup FreeVariables Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup Hiding Source #

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

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

Semigroup Overlappable Source #

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

Instance details

Defined in Agda.Syntax.Common

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

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

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

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

Semigroup MutualChecks Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Semigroup PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Semigroup Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

Semigroup NameMapEntry Source #

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

Instance details

Defined in Agda.Syntax.Scope.Base

Semigroup CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

Semigroup VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

Semigroup FlexRigMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup ReduceDefs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Semigroup Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Semigroup OccurrencesBuilder Source #

The semigroup laws only hold up to flattening of Concat.

Instance details

Defined in Agda.TypeChecking.Positivity

Semigroup ClausesPostChecks Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Def

Semigroup FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup AbsolutePath Source #

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

Instance details

Defined in Agda.Syntax.Position

Semigroup IntSet Source # 
Instance details

Defined in Agda.Utils.IntSet.Infinite

Semigroup MaxNat Source # 
Instance details

Defined in Agda.Utils.Monoid

Semigroup PartialOrdering Source #

Partial ordering forms a monoid under sequencing.

Instance details

Defined in Agda.Utils.PartialOrd

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

Defined in Data.ByteString.Builder.Internal

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Internal

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

Semigroup ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

Semigroup IntSet

Since: containers-0.5.7

Instance details

Defined in Data.IntSet.Internal

Semigroup Ordering

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

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

Defined in Text.PrettyPrint.HughesPJ

Methods

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

sconcat :: NonEmpty Doc -> Doc #

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

Semigroup ByteArray 
Instance details

Defined in Data.Primitive.ByteArray

Methods

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

sconcat :: NonEmpty ByteArray -> ByteArray #

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

Semigroup Series 
Instance details

Defined in Data.Aeson.Encoding.Internal

Semigroup Key 
Instance details

Defined in Data.Aeson.Key

Methods

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

sconcat :: NonEmpty Key -> Key #

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

Semigroup CalendarDiffDays

Additive

Instance details

Defined in Data.Time.Calendar.CalendarDiffDays

Semigroup CalendarDiffTime

Additive

Instance details

Defined in Data.Time.LocalTime.Internal.CalendarDiffTime

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

Defined in Data.Text.Short.Internal

Methods

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

sconcat :: NonEmpty ShortText -> ShortText #

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

Semigroup ()

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty () -> () #

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

Semigroup (DelayedMerge hl) Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Erased) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Quantity) Source #

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderComposition Relevance) Source #

Relevance forms a semigroup under composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (NotBlocked' t) 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.Blockers

Semigroup a => Semigroup (Range' a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

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

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

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

Semigroup (CallGraph cinfo) 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 (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 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 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 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 (TCM Doc) Source #

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

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

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

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

Semigroup (Match a) 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 #

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 #

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 a => Semigroup (RangeMap a) Source #

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

Instance details

Defined in Agda.Utils.RangeMap

Methods

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

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

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

Bits a => Semigroup (And a)

Since: base-4.16

Instance details

Defined in Data.Bits

Methods

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

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

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

FiniteBits a => Semigroup (Iff a)

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

Since: base-4.16

Instance details

Defined in Data.Bits

Methods

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

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

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

Bits a => Semigroup (Ior a)

Since: base-4.16

Instance details

Defined in Data.Bits

Methods

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

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

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

Bits a => Semigroup (Xor a)

Since: base-4.16

Instance details

Defined in Data.Bits

Methods

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

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

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

Semigroup a => Semigroup (Identity a)

Since: base-4.9.0.0

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

Since: base-4.11.0.0

Instance details

Defined in Data.Functor.Utils

Methods

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

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

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

Ord a => Semigroup (Min a)

Since: base-4.11.0.0

Instance details

Defined in Data.Functor.Utils

Methods

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

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

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

Semigroup (First a)

Since: base-4.9.0.0

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

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 #

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 #

Monoid m => Semigroup (WrappedMonoid m)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

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

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 #

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 #

Semigroup (PutM ()) 
Instance details

Defined in Data.Binary.Put

Methods

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

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

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

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

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 #

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

Defined in Data.CaseInsensitive.Internal

Methods

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

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

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

Semigroup (DNonEmpty a) 
Instance details

Defined in Data.DList.DNonEmpty.Internal

Methods

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

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

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

Semigroup (DList a) 
Instance details

Defined in Data.DList.Internal

Methods

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

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

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

Semigroup a => Semigroup (IO a)

Since: base-4.10.0.0

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 #

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

Defined in Data.Aeson.KeyMap

Methods

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

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

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

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

Defined in Data.Strict.Maybe

Methods

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

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

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

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

Since: template-haskell-2.17.0.0

Instance details

Defined in Language.Haskell.TH.Syntax

Methods

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

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

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

Semigroup (Vector a) 
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 #

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

Since: base-4.15

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup [a]

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

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 #

Semigroup a => Semigroup (Blocked' t a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

Methods

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

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

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

(Monad m, Semigroup a) => Semigroup (PureConversionT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

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

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

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 #

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

Defined in Data.Strict.Either

Methods

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

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

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

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

Defined in Data.Strict.These

Methods

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

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

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

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

Defined in Data.Strict.Tuple

Methods

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

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

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

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

Defined in Data.These

Methods

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

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

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

Semigroup (Parser i a) 
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 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 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 (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 #

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

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

Defined in Agda.Utils.Semigroup

Methods

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

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

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

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

Defined in Agda.Utils.Semigroup

Methods

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

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

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

(Semigroup a, Semigroup 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 (f a), Semigroup (g a)) => Semigroup (Product f g a)

Since: base-4.16.0.0

Instance details

Defined in Data.Functor.Product

Methods

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

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

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

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

Since: base-4.12.0.0

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

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

Since: base-4.16.0.0

Instance details

Defined in Data.Functor.Compose

Methods

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

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

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

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

Since: base-4.12.0.0

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

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

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

Orphan instances

Semigroup (TCM Doc) Source #

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

Instance details

Methods

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

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

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