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

Agda.TypeChecking.Pretty

Synopsis

Documentation

newtype PrettyContext Source #

Constructors

PrettyContext Context 

Instances

Instances details
PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

class PrettyTCM a where Source #

Methods

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

Instances

Instances details
PrettyTCM Bool Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM String Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Range Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Relevance Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Quantity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Modality Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Nat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM QName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Name Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Literal Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM AbstractName Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Blocker Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Clause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Level Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Sort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Type Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Term Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM TypedBinding Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Expr Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM NegativeUnification Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

PrettyTCM CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

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

Defined in Agda.TypeChecking.Pretty

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Constraint

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Constraint

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM PrettyContext Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM NamedClause Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM ElimType Source # 
Instance details

Defined in Agda.TypeChecking.Records

PrettyTCM LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AnnotationPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

PrettyTCM Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

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

PrettyTCM SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

PrettyTCM HypSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM SizeConstraint Source #

Assumes we are in the right context.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

PrettyTCM ErrorPart Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

PrettyTCM SplitClause Source #

For debugging only.

Instance details

Defined in Agda.TypeChecking.Coverage

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Seq OccursWhere) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM (NamedArg Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (NamedArg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Named_ Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Arg Bool) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg Bool -> 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 Term) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Arg Expr) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (QNamed Clause) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM (LHSState a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

PrettyTCM a => PrettyTCM (Masked a) Source #

Print masked things in double parentheses.

Instance details

Defined in Agda.Termination.Monad

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

(PrettyTCM n, 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 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 Ordering

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Semigroup ()

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty () -> () #

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

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Internal

Semigroup ByteString 
Instance details

Defined in Data.ByteString.Lazy.Internal

Semigroup Builder 
Instance details

Defined in Data.ByteString.Builder.Internal

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

Defined in Data.Attoparsec.Internal.Types

Methods

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

sconcat :: NonEmpty More -> More #

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

Semigroup Void

Since: base-4.9.0.0

Instance details

Defined in Data.Void

Methods

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

sconcat :: NonEmpty Void -> Void #

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

Semigroup All

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty All -> All #

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

Semigroup Any

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

sconcat :: NonEmpty Any -> Any #

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

Semigroup ShortByteString 
Instance details

Defined in Data.ByteString.Short.Internal

Semigroup AttributeValue 
Instance details

Defined in Text.Blaze.Internal

Semigroup Attribute 
Instance details

Defined in Text.Blaze.Internal

Semigroup ChoiceString 
Instance details

Defined in Text.Blaze.Internal

Semigroup IntSet

Since: containers-0.5.7

Instance details

Defined in Data.IntSet.Internal

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

Semigroup ShortText 
Instance details

Defined in Data.Text.Short.Internal

Semigroup CalendarDiffTime

Additive

Instance details

Defined in Data.Time.LocalTime.Internal.CalendarDiffTime

Semigroup CalendarDiffDays

Additive

Instance details

Defined in Data.Time.Calendar.CalendarDiffDays

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

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

Instance details

Defined in Agda.Syntax.Position

Semigroup ExpandedEllipsis Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup CoverageCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup PositivityCheck Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup IsAbstract Source #

Semigroup computes if any of several is an AbstractDef.

Instance details

Defined in Agda.Syntax.Common

Semigroup FreeVariables Source # 
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 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 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 Hiding Source #

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

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

Defined in Agda.Compiler.JS.Syntax

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

Defined in Agda.Syntax.Concrete.Definitions.Types

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

Defined in Agda.Syntax.Info

Semigroup PositionMap Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup TokenBased Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup DefinitionSite Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Precise

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

NameKind in Name can get more precise.

Instance details

Defined in Agda.Interaction.Highlighting.Precise

Semigroup Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

Semigroup FlexRigMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup MetaSet Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

Semigroup ReduceDefs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Semigroup Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.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 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 LeftoverPatterns Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup OccurrencesBuilder Source #

The semigroup laws only hold up to flattening of Concat.

Instance details

Defined in Agda.TypeChecking.Positivity

Semigroup CallPath Source # 
Instance details

Defined in Agda.Termination.Monad

Semigroup ClausesPostChecks Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Def

Semigroup IsMain Source #

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Semigroup HsCompileState Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

Semigroup UsesFloat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Compiler

Semigroup [a]

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (Maybe a)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (IO a)

Since: base-4.10.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup p => Semigroup (Par1 p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: Par1 p -> Par1 p -> Par1 p #

sconcat :: NonEmpty (Par1 p) -> Par1 p #

stimes :: Integral b => b -> Par1 p -> Par1 p #

Semigroup a => Semigroup (Solo a) 
Instance details

Defined in Data.Tuple.Solo

Methods

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

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

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

Semigroup (IResult a) 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

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

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

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

Semigroup (Result a) 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

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

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

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

Semigroup (Parser a) 
Instance details

Defined in Data.Aeson.Types.Internal

Methods

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

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

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

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

Only defined by async for base >= 4.9

Since: async-2.1.0

Instance details

Defined in Control.Concurrent.Async

Ord a => Semigroup (Min a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

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

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

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

Ord a => Semigroup (Max a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

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

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

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

Semigroup (First a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

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

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

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

Semigroup (Last a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

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

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

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

Monoid m => Semigroup (WrappedMonoid m)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Semigroup a => Semigroup (Option a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup

Methods

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

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

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

Semigroup a => Semigroup (Identity a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Identity

Methods

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

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

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

Semigroup (First a)

Since: base-4.9.0.0

Instance details

Defined in Data.Monoid

Methods

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

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

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

Semigroup (Last a)

Since: base-4.9.0.0

Instance details

Defined in Data.Monoid

Methods

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

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

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

Semigroup a => Semigroup (Dual a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Semigroup (Endo a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Num a => Semigroup (Sum a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Num a => Semigroup (Product a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

Semigroup a => Semigroup (Down a)

Since: base-4.11.0.0

Instance details

Defined in Data.Ord

Methods

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

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

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

Semigroup (NonEmpty a)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup (PutM ()) 
Instance details

Defined in Data.Binary.Put

Methods

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

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

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

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

Since: containers-0.5.7

Instance details

Defined in Data.IntMap.Internal

Methods

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

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

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

Semigroup (Seq a)

Since: containers-0.5.7

Instance details

Defined in Data.Sequence.Internal

Methods

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

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

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

Ord a => Semigroup (Set a)

Since: containers-0.5.7

Instance details

Defined in Data.Set.Internal

Methods

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

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

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

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

Since: primitive-0.6.4.0

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)

Since: primitive-0.6.3.0

Instance details

Defined in Data.Primitive.SmallArray

Semigroup (Array a)

Since: primitive-0.6.3.0

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

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

<> = union

O(n+m)

To obtain good performance, the smaller set must be presented as the first argument.

Examples

Expand
>>> fromList [1,2] <> fromList [2,3]
fromList [1,2,3]
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 #

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 #

Prim a => Semigroup (Vector a) 
Instance details

Defined in Data.Vector.Primitive

Methods

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

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

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

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

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

Defined in Agda.Utils.Bag

Methods

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

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

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

Semigroup 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 (UnderComposition Cohesion) Source #

Cohesion forms a semigroup under composition.

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 (UnderComposition Erased) Source # 
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 Modality) Source #

Pointwise composition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Cohesion) Source #

Cohesion forms a semigroup under addition.

Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Relevance) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Quantity) Source # 
Instance details

Defined in Agda.Syntax.Common

Semigroup (UnderAddition Modality) Source #

Pointwise addition.

Instance details

Defined in Agda.Syntax.Common

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

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

Defined in Agda.Interaction.Highlighting.Precise

Semigroup (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

(<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo #

sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo #

stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo #

Semigroup (CallGraph cinfo) Source #

CallGraph is a monoid under union.

Instance details

Defined in Agda.Termination.CallGraph

Methods

(<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo #

sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo #

stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo #

Semigroup (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 (VarMap' a) Source #

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

Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

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

Semigroup a => Semigroup (VarOcc' a) Source #

The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair (t₁,t₂) then and t₁ has o₁ the occurrences of a variable x and t₂ has o₂ the occurrences of the same variable, then (t₁,t₂) has mappend o₁ o₂ occurrences of that variable.

From counting Quantity, we extrapolate this to FlexRig and Relevance: we care most about about StronglyRigid Relevant occurrences. E.g., if t₁ has a StronglyRigid occurrence and t₂ a Flexible occurrence, then (t₁,t₂) still has a StronglyRigid occurrence. Analogously, Relevant occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant.

VarOcc forms a semiring, and this monoid is the addition of the semiring.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

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

Semigroup m => Semigroup (Case m) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

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

sconcat :: NonEmpty (Case m) -> Case m #

stimes :: Integral b => b -> Case m -> Case m #

Semigroup c => Semigroup (WithArity c) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

(<>) :: WithArity c -> WithArity c -> WithArity c #

sconcat :: NonEmpty (WithArity c) -> WithArity c #

stimes :: Integral b => b -> WithArity c -> WithArity c #

Semigroup (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

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

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

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

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

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup (Either a b)

Since: base-4.9.0.0

Instance details

Defined in Data.Either

Methods

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

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

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

Semigroup (V1 p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: V1 p -> V1 p -> V1 p #

sconcat :: NonEmpty (V1 p) -> V1 p #

stimes :: Integral b => b -> V1 p -> V1 p #

Semigroup (U1 p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: U1 p -> U1 p -> U1 p #

sconcat :: NonEmpty (U1 p) -> U1 p #

stimes :: Integral b => b -> U1 p -> U1 p #

(Semigroup a, Semigroup b) => Semigroup (a, b)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (ST s a)

Since: base-4.11.0.0

Instance details

Defined in GHC.ST

Methods

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

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

stimes :: Integral b => b -> ST s a -> ST s a #

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)

<> = union

If a key occurs in both maps, the mapping from the first will be the mapping in the result.

Examples

Expand
>>> fromList [(1,'a'),(2,'b')] <> fromList [(2,'c'),(3,'d')]
fromList [(1,'a'),(2,'b'),(3,'d')]
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 (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 (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 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 (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.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 (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 #

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

Defined in Agda.Utils.ListT

Methods

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

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

stimes :: Integral b => b -> ListT m a -> ListT m a #

Semigroup (Using' n m) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

(<>) :: Using' n m -> Using' n m -> Using' n m #

sconcat :: NonEmpty (Using' n m) -> Using' n m #

stimes :: Integral b => b -> Using' n m -> Using' n m #

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

Defined in Agda.Syntax.Common

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

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

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

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

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

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

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

(Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

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

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

Semigroup a => Semigroup (Const a b)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Const

Methods

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

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

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

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

Since: base-4.12.0.0

Instance details

Defined in Data.Monoid

Methods

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

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

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

Alternative f => Semigroup (Alt f a)

Since: base-4.9.0.0

Instance details

Defined in Data.Semigroup.Internal

Methods

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

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

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

(Applicative m, Semigroup 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 (Tagged s a) 
Instance details

Defined in Data.Tagged

Methods

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

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

stimes :: Integral b => b -> Tagged s a -> Tagged s a #

Semigroup c => Semigroup (K1 i c p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: K1 i c p -> K1 i c p -> K1 i c p #

sconcat :: NonEmpty (K1 i c p) -> K1 i c p #

stimes :: Integral b => b -> K1 i c p -> K1 i c p #

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

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p #

sconcat :: NonEmpty ((f :*: g) p) -> (f :*: g) p #

stimes :: Integral b => b -> (f :*: g) p -> (f :*: g) p #

(Semigroup a, Semigroup b, Semigroup c, Semigroup d) => Semigroup (a, b, c, d)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

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

sconcat :: NonEmpty (a, b, c, d) -> (a, b, c, d) #

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

Semigroup (f p) => Semigroup (M1 i c f p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: M1 i c f p -> M1 i c f p -> M1 i c f p #

sconcat :: NonEmpty (M1 i c f p) -> M1 i c f p #

stimes :: Integral b => b -> M1 i c f p -> M1 i c f p #

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

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: (f :.: g) p -> (f :.: g) p -> (f :.: g) p #

sconcat :: NonEmpty ((f :.: g) p) -> (f :.: g) p #

stimes :: Integral b => b -> (f :.: g) p -> (f :.: g) p #

(Semigroup a, Semigroup b, Semigroup c, Semigroup d, Semigroup e) => Semigroup (a, b, c, d, e)

Since: base-4.9.0.0

Instance details

Defined in GHC.Base

Methods

(<>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) #

sconcat :: NonEmpty (a, b, c, d, e) -> (a, b, c, d, e) #

stimes :: Integral b0 => b0 -> (a, b, c, d, e) -> (a, b, c, d, e) #

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 #