Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Pretty

Synopsis

Documentation

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

PrettyTCM NamedClause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

PrettyTCM SplitClause Source #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

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

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

PrettyTCM UnifyState Source # 
Instance details

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

PrettyTCM UnifyStep Source # 
Instance details

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

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

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

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

Methods

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

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 #

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

Defined in Agda.Interaction.BasicOps

Methods

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

type Doc = Doc Source #

newtype PrettyContext Source #

Constructors

PrettyContext Context 

Instances

Instances details
PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a 

class PrettyTCMWithNode a where Source #

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

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

text :: Applicative m => String -> 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 #

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

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

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

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

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

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

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

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

comma :: Applicative m => m Doc Source #

colon :: Applicative m => m Doc Source #

equals :: Applicative m => m Doc Source #

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

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

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

prettyList without the brackets.

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

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

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

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

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

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

Comma-separated list in brackets.

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

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

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

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

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

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

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

Pretty print with a given context precedence

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

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

Proper pretty printing of patterns:

class Semigroup a where #

Minimal complete definition

(<>) | sconcat

Methods

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

Instances

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

Methods

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

sconcat :: NonEmpty Comment -> Comment

stimes :: Integral b => b -> Comment -> Comment

Semigroup HsCompileState Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

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

Semigroup PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup OptionsPragma Source # 
Instance details

Defined in Agda.Interaction.Library.Base

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

Methods

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

sconcat :: NonEmpty Hiding -> Hiding

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

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

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

Methods

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

sconcat :: NonEmpty Q0Origin -> Q0Origin

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

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

NameKind in Name can get more precise.

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

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

sconcat :: NonEmpty Aspect -> Aspect

stimes :: Integral b => b -> Aspect -> Aspect

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

Methods

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

sconcat :: NonEmpty NameKind -> NameKind

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

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup MutualChecks Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Semigroup PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

sconcat :: NonEmpty PatInfo -> PatInfo

stimes :: Integral b => b -> PatInfo -> PatInfo

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

Methods

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

sconcat :: NonEmpty CallPath -> CallPath

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

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

Methods

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

sconcat :: NonEmpty MetaSet -> MetaSet

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

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

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

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

Semigroup ByteArray 
Instance details

Defined in Data.Array.Byte

Methods

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

sconcat :: NonEmpty ByteArray -> ByteArray

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

Semigroup All 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty All -> All

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

Semigroup Any 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty Any -> Any

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

Semigroup Void 
Instance details

Defined in GHC.Base

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

Methods

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

sconcat :: NonEmpty Builder -> Builder

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

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Internal.Type

Methods

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

sconcat :: NonEmpty ByteString -> ByteString

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

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

Methods

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

sconcat :: NonEmpty ByteString -> ByteString

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

Semigroup ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

Methods

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

sconcat :: NonEmpty ShortByteString -> ShortByteString

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

Semigroup IntSet 
Instance details

Defined in Data.IntSet.Internal

Methods

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

sconcat :: NonEmpty IntSet -> IntSet

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

Semigroup OsString 
Instance details

Defined in System.OsString.Internal.Types

Methods

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

sconcat :: NonEmpty OsString -> OsString

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

Semigroup PosixString 
Instance details

Defined in System.OsString.Internal.Types

Methods

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

sconcat :: NonEmpty PosixString -> PosixString

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

Semigroup WindowsString 
Instance details

Defined in System.OsString.Internal.Types

Methods

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

sconcat :: NonEmpty WindowsString -> WindowsString

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

Semigroup Ordering 
Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty Ordering -> Ordering

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

Semigroup Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

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

sconcat :: NonEmpty Doc -> Doc

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

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

Defined in Data.Aeson.Key

Methods

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

sconcat :: NonEmpty Key -> Key

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

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

Methods

(<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl #

sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl

stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl

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

Methods

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

sconcat :: NonEmpty (NotBlocked' t) -> NotBlocked' t

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

Eq a => Semigroup (Range' a) 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 (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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

SmallSetElement a => Semigroup (SmallSet a) Source # 
Instance details

Defined in Agda.Utils.SmallSet

Methods

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

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

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

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

Defined in Data.Monoid

Methods

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

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

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

Semigroup (Last a) 
Instance details

Defined in Data.Monoid

Methods

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

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

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

Semigroup a => Semigroup (Down a) 
Instance details

Defined in Data.Ord

Methods

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

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

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

Semigroup (First a) 
Instance details

Defined in Data.Semigroup

Methods

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

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

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

Semigroup (Last a) 
Instance details

Defined in Data.Semigroup

Methods

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

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

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

Ord a => Semigroup (Max a) 
Instance details

Defined in Data.Semigroup

Methods

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

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

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

Ord a => Semigroup (Min a) 
Instance details

Defined in Data.Semigroup

Methods

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

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

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

Monoid m => Semigroup (WrappedMonoid m) 
Instance details

Defined in Data.Semigroup

Methods

(<>) :: WrappedMonoid m -> WrappedMonoid m -> WrappedMonoid m #

sconcat :: NonEmpty (WrappedMonoid m) -> WrappedMonoid m

stimes :: Integral b => b -> WrappedMonoid m -> WrappedMonoid m

Semigroup a => Semigroup (Dual a) 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Semigroup (Endo a) 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Num a => Semigroup (Product a) 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Num a => Semigroup (Sum a) 
Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Semigroup (NonEmpty a) 
Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (STM a) 
Instance details

Defined in GHC.Conc.Sync

Methods

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

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

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

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

Defined in GHC.Generics

Methods

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

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

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

Semigroup p => Semigroup (Par1 p) 
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

Num a => Semigroup (AlphaColour a) 
Instance details

Defined in Data.Colour.Internal

Methods

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

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

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

Num a => Semigroup (Colour a) 
Instance details

Defined in Data.Colour.Internal

Methods

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

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

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

Semigroup (IntMap a) 
Instance details

Defined in Data.IntMap.Internal

Methods

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

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

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

Semigroup (Seq a) 
Instance details

Defined in Data.Sequence.Internal

Methods

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

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

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

Ord a => Semigroup (Intersection a) 
Instance details

Defined in Data.Set.Internal

Methods

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

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

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

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

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (a) 
Instance details

Defined in GHC.Base

Methods

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

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

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

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

Defined in GHC.Base

Methods

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

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

stimes :: Integral b0 => b0 -> (a, b) -> (a, b)

Semigroup b => Semigroup (a -> b) 
Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (Const a b) 
Instance details

Defined in Data.Functor.Const

Methods

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

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

stimes :: Integral b0 => b0 -> Const a b -> Const a b

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

Defined in Data.Monoid

Methods

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

sconcat :: NonEmpty (Ap f a) -> Ap f a

stimes :: Integral b => b -> Ap f a -> Ap f a

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

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty (Alt f a) -> Alt f a

stimes :: Integral b => b -> Alt f a -> Alt f a

Semigroup (f p) => Semigroup (Rec1 f p) 
Instance details

Defined in GHC.Generics

Methods

(<>) :: Rec1 f p -> Rec1 f p -> Rec1 f p #

sconcat :: NonEmpty (Rec1 f p) -> Rec1 f p

stimes :: Integral b => b -> Rec1 f p -> Rec1 f p

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

Defined in Data.Functor.Constant

Methods

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

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

stimes :: Integral b0 => b0 -> Constant a b -> Constant a b

(Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c) 
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) 
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) 
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) 
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) 
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) 
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) 
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) 
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) 
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 = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #

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

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