Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Pretty

Contents

Orphan instances

Synopsis

newtype PrettyContext = PrettyContext Context
class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> m Doc
type MonadPretty m = (MonadReify m, MonadAbsToCon m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
pretty :: (Applicative m, Pretty a) => a -> m Doc
nest :: Functor m => Int -> m Doc -> m Doc
($$) :: Applicative m => m Doc -> m Doc -> m Doc
(<+>) :: Applicative m => m Doc -> m Doc -> m Doc
(<?>) :: Applicative m => m Doc -> m Doc -> m Doc
hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
text :: Applicative m => String -> m Doc
class PrettyTCMWithNode a where
- prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
data WithNode n a = WithNode n a
type Doc = Doc
comma :: Applicative m => m Doc
colon :: Applicative m => m Doc
equals :: Applicative m => m Doc
prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
multiLineText :: Applicative m => String -> m Doc
pwords :: Applicative m => String -> [m Doc]
fwords :: Applicative m => String -> m Doc
hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
($+$) :: Applicative m => m Doc -> m Doc -> m Doc
braces :: Functor m => m Doc -> m Doc
dbraces :: Functor m => m Doc -> m Doc
brackets :: Functor m => m Doc -> m Doc
parens :: Functor m => m Doc -> m Doc
parensNonEmpty :: Functor m => m Doc -> m Doc
doubleQuotes :: Functor m => m Doc -> m Doc
quotes :: Functor m => m Doc -> m Doc
pshow :: (Applicative m, Show a) => a -> m Doc
prettyList :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
class Semigroup a where
- (<>) :: a -> a -> a
type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m)

Documentation

newtype PrettyContext Source #

Constructors

PrettyContext Context

Instances

Instances details

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

class PrettyTCM a where Source #

Methods

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

Instances

Instances details

PrettyTCM Expr Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
PrettyTCM ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
PrettyTCM TypedBinding Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
PrettyTCM ModuleName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ModuleName -> m Doc Source #
PrettyTCM Name Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Name -> m Doc Source #
PrettyTCM QName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => QName -> m Doc Source #
PrettyTCM MetaId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
PrettyTCM Modality Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Modality -> m Doc Source #
PrettyTCM Nat Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Nat -> m Doc Source #
PrettyTCM ProblemId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
PrettyTCM Quantity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Quantity -> m Doc Source #
PrettyTCM Relevance Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Relevance -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => DBPatVar -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => EqualityView -> m Doc Source #
PrettyTCM Level Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Level -> m Doc Source #
PrettyTCM Sort Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Sort -> m Doc Source #
PrettyTCM Telescope Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Telescope -> m Doc Source #
PrettyTCM 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 Methods prettyTCM :: MonadPretty m => AbstractName -> m Doc Source #
PrettyTCM NamedClause Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
PrettyTCM SplitClause Source #	For debugging only.
Instance details Defined in Agda.TypeChecking.Coverage Methods prettyTCM :: MonadPretty m => SplitClause -> m Doc Source #
PrettyTCM SplitPatVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods prettyTCM :: MonadPretty m => SplitPatVar -> m Doc Source #
PrettyTCM SplitTag Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => SplitTag -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => CallInfo -> m Doc Source #
PrettyTCM Candidate Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Candidate -> m Doc Source #
PrettyTCM CheckpointId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CheckpointId -> m Doc Source #
PrettyTCM CompareAs Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => CompareAs -> m Doc Source #
PrettyTCM Comparison Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #
PrettyTCM Constraint Source #
Instance details Defined in Agda.TypeChecking.Pretty.Constraint Methods prettyTCM :: MonadPretty m => Constraint -> m Doc Source #
PrettyTCM DisplayTerm Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => DisplayTerm -> m Doc Source #
PrettyTCM IsForced Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => IsForced -> m Doc Source #
PrettyTCM NLPSort Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NLPSort -> m Doc Source #
PrettyTCM NLPType Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NLPType -> m Doc Source #
PrettyTCM NLPat Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NLPat -> m Doc Source #
PrettyTCM NegativeUnification Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => NegativeUnification -> m Doc Source #
PrettyTCM Polarity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Polarity -> m Doc Source #
PrettyTCM ProblemConstraint Source #
Instance details Defined in Agda.TypeChecking.Pretty.Constraint Methods prettyTCM :: MonadPretty m => ProblemConstraint -> m Doc Source #
PrettyTCM RewriteRule Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => RewriteRule -> m Doc Source #
PrettyTCM SplitError Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => SplitError -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => TCWarning -> m Doc Source #
PrettyTCM TypeCheckingProblem Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypeCheckingProblem -> m Doc Source #
PrettyTCM TypeError Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TypeError -> m Doc Source #
PrettyTCM UnificationFailure Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => UnificationFailure -> m Doc Source #
PrettyTCM 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 Methods prettyTCM :: MonadPretty m => Occurrence -> m Doc Source #
PrettyTCM PrettyContext Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => PrettyContext -> m Doc Source #
PrettyTCM ElimType Source #
Instance details Defined in Agda.TypeChecking.Records Methods prettyTCM :: MonadPretty m => ElimType -> m Doc Source #
PrettyTCM AbsurdPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source #
PrettyTCM AnnotationPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc Source #
PrettyTCM AsBinding Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AsBinding -> m Doc Source #
PrettyTCM DotPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => DotPattern -> m Doc Source #
PrettyTCM LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source #
PrettyTCM HypSizeConstraint Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => HypSizeConstraint -> m Doc Source #
PrettyTCM SizeConstraint Source #	Assumes we are in the right context.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeConstraint -> m Doc Source #
PrettyTCM SizeMeta Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods prettyTCM :: MonadPretty m => SizeMeta -> m Doc Source #
PrettyTCM ErrorPart Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods prettyTCM :: MonadPretty m => ErrorPart -> m Doc Source #
PrettyTCM Permutation Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Permutation -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #
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 Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
PrettyTCM (NamedArg Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Term -> m Doc Source #
PrettyTCM (Named_ Term) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Named_ Term -> 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 a => PrettyTCM (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocked a -> m Doc Source #
PrettyTCM (Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #
PrettyTCM (Dom (Name, Type)) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Dom (Name, Type) -> m Doc Source #
PrettyTCM a => PrettyTCM (Pattern' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern' a -> m Doc Source #
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #
PrettyTCM (Type' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Type' NLPat -> m Doc Source #
PrettyTCM (Elim' DisplayTerm) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' DisplayTerm -> m Doc Source #
PrettyTCM (Elim' NLPat) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Elim' NLPat -> 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 (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 Methods prettyTCM :: MonadPretty m => MaybeReduced 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 (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 #
(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 MonadPretty m = (MonadReify m, MonadAbsToCon m, IsString (m Doc), Null (m Doc), Semigroup (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 #

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

class PrettyTCMWithNode a where Source #

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

Methods

prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc Source #

Instances

Instances details

PrettyTCMWithNode Occurrence Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n Occurrence -> m Doc Source #
PrettyTCMWithNode (Edge OccursWhere) Source #
Instance details Defined in Agda.TypeChecking.Positivity Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge OccursWhere) -> m Doc Source #

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a

type Doc = Doc Source #

comma :: Applicative m => m Doc Source #

colon :: Applicative m => m Doc Source #

equals :: Applicative m => m Doc Source #

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

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

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

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

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

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

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

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:

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

class Semigroup a where #

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

Instances should satisfy the following:

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

Since: base-4.9.0.0

Methods

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

An associative operation.

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

Instances

Instances details

Semigroup 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 UsesFloat Source #
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods (<>) :: UsesFloat -> UsesFloat -> UsesFloat # sconcat :: NonEmpty UsesFloat -> UsesFloat # stimes :: Integral b => b -> UsesFloat -> UsesFloat #
Semigroup HsCompileState Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState # sconcat :: NonEmpty HsCompileState -> HsCompileState # stimes :: Integral b => b -> HsCompileState -> HsCompileState #
Semigroup Occurs Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: Occurs -> Occurs -> Occurs # sconcat :: NonEmpty Occurs -> Occurs # stimes :: Integral b => b -> Occurs -> Occurs #
Semigroup SeqArg Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: SeqArg -> SeqArg -> SeqArg # sconcat :: NonEmpty SeqArg -> SeqArg # stimes :: Integral b => b -> SeqArg -> SeqArg #
Semigroup UnderLambda Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: UnderLambda -> UnderLambda -> UnderLambda # sconcat :: NonEmpty UnderLambda -> UnderLambda # stimes :: Integral b => b -> UnderLambda -> UnderLambda #
Semigroup Aspect Source #	`NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Interaction.Highlighting.Precise 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 Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite # stimes :: Integral b => b -> DefinitionSite -> DefinitionSite #
Semigroup NameKind Source #	Some `NameKind`s are more informative than others.
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: NameKind -> NameKind -> NameKind # sconcat :: NonEmpty NameKind -> NameKind # stimes :: Integral b => b -> NameKind -> NameKind #
Semigroup PositionMap Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: PositionMap -> PositionMap -> PositionMap # sconcat :: NonEmpty PositionMap -> PositionMap # stimes :: Integral b => b -> PositionMap -> PositionMap #
Semigroup TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased # stimes :: Integral b => b -> TokenBased -> TokenBased #
Semigroup CoverageCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck #
Semigroup ExpandedEllipsis Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis # stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis #
Semigroup FreeVariables Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables # stimes :: Integral b => b -> FreeVariables -> FreeVariables #
Semigroup 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 Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract # sconcat :: NonEmpty IsAbstract -> IsAbstract # stimes :: Integral b => b -> IsAbstract -> IsAbstract #
Semigroup Overlappable Source #	Just for the `Hiding` instance. Should never combine different overlapping.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable # stimes :: Integral b => b -> Overlappable -> Overlappable #
Semigroup PositivityCheck Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck #
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 Methods (<>) :: QωOrigin -> QωOrigin -> QωOrigin # sconcat :: NonEmpty QωOrigin -> QωOrigin # stimes :: Integral b => b -> QωOrigin -> QωOrigin #
Semigroup MutualChecks Source #
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (<>) :: MutualChecks -> MutualChecks -> MutualChecks # sconcat :: NonEmpty MutualChecks -> MutualChecks # stimes :: Integral b => b -> MutualChecks -> MutualChecks #
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 Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (<>) :: Blocker -> Blocker -> Blocker # sconcat :: NonEmpty Blocker -> Blocker # stimes :: Integral b => b -> Blocker -> Blocker #
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 Methods (<>) :: NameMapEntry -> NameMapEntry -> NameMapEntry # sconcat :: NonEmpty NameMapEntry -> NameMapEntry # stimes :: Integral b => b -> NameMapEntry -> NameMapEntry #
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 Methods (<>) :: VarCounts -> VarCounts -> VarCounts # sconcat :: NonEmpty VarCounts -> VarCounts # stimes :: Integral b => b -> VarCounts -> VarCounts #
Semigroup FlexRigMap Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: FlexRigMap -> FlexRigMap -> FlexRigMap # sconcat :: NonEmpty FlexRigMap -> FlexRigMap # stimes :: Integral b => b -> FlexRigMap -> FlexRigMap #
Semigroup MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: MetaSet -> MetaSet -> MetaSet # sconcat :: NonEmpty MetaSet -> MetaSet # stimes :: Integral b => b -> MetaSet -> MetaSet #
Semigroup ReduceDefs Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: ReduceDefs -> ReduceDefs -> ReduceDefs # sconcat :: NonEmpty ReduceDefs -> ReduceDefs # stimes :: Integral b => b -> ReduceDefs -> ReduceDefs #
Semigroup Simplification Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: Simplification -> Simplification -> Simplification # sconcat :: NonEmpty Simplification -> Simplification # stimes :: Integral b => b -> Simplification -> Simplification #
Semigroup OccurrencesBuilder Source #	The semigroup laws only hold up to flattening of `Concat`.
Instance details Defined in Agda.TypeChecking.Positivity Methods (<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder # sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder # stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder #
Semigroup ClausesPostChecks Source #
Instance details Defined in Agda.TypeChecking.Rules.Def Methods (<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks # sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks # stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks #
Semigroup FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: FlexChoice -> FlexChoice -> FlexChoice # sconcat :: NonEmpty FlexChoice -> FlexChoice # stimes :: Integral b => b -> FlexChoice -> FlexChoice #
Semigroup LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns # stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns #
Semigroup AbsolutePath Source #	To get `Semigroup Range'`, we need a semigroup instance for `AbsolutePath`.
Instance details Defined in Agda.Syntax.Position Methods (<>) :: AbsolutePath -> AbsolutePath -> AbsolutePath # sconcat :: NonEmpty AbsolutePath -> AbsolutePath # stimes :: Integral b => b -> AbsolutePath -> AbsolutePath #
Semigroup IntSet Source #
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (<>) :: IntSet -> IntSet -> IntSet # sconcat :: NonEmpty IntSet -> IntSet # stimes :: Integral b => b -> IntSet -> IntSet #
Semigroup MaxNat Source #
Instance details Defined in Agda.Utils.Monoid Methods (<>) :: MaxNat -> MaxNat -> MaxNat # sconcat :: NonEmpty MaxNat -> MaxNat # stimes :: Integral b => b -> MaxNat -> MaxNat #
Semigroup PartialOrdering Source #	Partial ordering forms a monoid under sequencing.
Instance details Defined in Agda.Utils.PartialOrd Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering # sconcat :: NonEmpty PartialOrdering -> PartialOrdering # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering #
Semigroup All	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: All -> All -> All # sconcat :: NonEmpty All -> All # stimes :: Integral b => b -> All -> All #
Semigroup Any	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Any -> Any -> Any # sconcat :: NonEmpty Any -> Any # stimes :: Integral b => b -> Any -> Any #
Semigroup Void	Since: base-4.9.0.0
Instance details Defined in Data.Void Methods (<>) :: Void -> Void -> Void # sconcat :: NonEmpty Void -> Void # stimes :: Integral b => b -> Void -> Void #
Semigroup Attribute
Instance details Defined in Text.Blaze.Internal Methods (<>) :: Attribute -> Attribute -> Attribute # sconcat :: NonEmpty Attribute -> Attribute # stimes :: Integral b => b -> Attribute -> Attribute #
Semigroup AttributeValue
Instance details Defined in Text.Blaze.Internal Methods (<>) :: AttributeValue -> AttributeValue -> AttributeValue # sconcat :: NonEmpty AttributeValue -> AttributeValue # stimes :: Integral b => b -> AttributeValue -> AttributeValue #
Semigroup ChoiceString
Instance details Defined in Text.Blaze.Internal Methods (<>) :: ChoiceString -> ChoiceString -> ChoiceString # sconcat :: NonEmpty ChoiceString -> ChoiceString # stimes :: Integral b => b -> ChoiceString -> ChoiceString #
Semigroup Builder
Instance details Defined in Data.ByteString.Builder.Internal Methods (<>) :: Builder -> Builder -> Builder # sconcat :: NonEmpty Builder -> Builder # stimes :: Integral b => b -> Builder -> Builder #
Semigroup ByteString
Instance details Defined in Data.ByteString.Internal Methods (<>) :: ByteString -> ByteString -> ByteString # sconcat :: NonEmpty ByteString -> ByteString # stimes :: Integral b => b -> ByteString -> ByteString #
Semigroup ByteString
Instance details Defined in Data.ByteString.Lazy.Internal Methods (<>) :: ByteString -> ByteString -> ByteString # sconcat :: NonEmpty ByteString -> ByteString # stimes :: Integral b => b -> ByteString -> ByteString #
Semigroup 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	Since: containers-0.5.7
Instance details Defined in Data.IntSet.Internal Methods (<>) :: IntSet -> IntSet -> IntSet # sconcat :: NonEmpty IntSet -> IntSet # stimes :: Integral b => b -> IntSet -> IntSet #
Semigroup Ordering	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: Ordering -> Ordering -> Ordering # sconcat :: NonEmpty Ordering -> Ordering # stimes :: Integral b => b -> Ordering -> Ordering #
Semigroup Slot
Instance details Defined in Data.HashTable.ST.Basic Methods (<>) :: Slot -> Slot -> Slot # sconcat :: NonEmpty Slot -> Slot # stimes :: Integral b => b -> Slot -> Slot #
Semigroup Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (<>) :: Doc -> Doc -> Doc # sconcat :: NonEmpty Doc -> Doc # stimes :: Integral b => b -> Doc -> Doc #
Semigroup ByteArray
Instance details Defined in Data.Primitive.ByteArray Methods (<>) :: ByteArray -> ByteArray -> ByteArray # sconcat :: NonEmpty ByteArray -> ByteArray # stimes :: Integral b => b -> ByteArray -> ByteArray #
Semigroup Series
Instance details Defined in Data.Aeson.Encoding.Internal 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 CalendarDiffDays	Additive
Instance details Defined in Data.Time.Calendar.CalendarDiffDays Methods (<>) :: CalendarDiffDays -> CalendarDiffDays -> CalendarDiffDays # sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays # stimes :: Integral b => b -> CalendarDiffDays -> CalendarDiffDays #
Semigroup CalendarDiffTime	Additive
Instance details Defined in Data.Time.LocalTime.Internal.CalendarDiffTime Methods (<>) :: CalendarDiffTime -> CalendarDiffTime -> CalendarDiffTime # sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime # stimes :: Integral b => b -> CalendarDiffTime -> CalendarDiffTime #
Semigroup More
Instance details Defined in Data.Attoparsec.Internal.Types Methods (<>) :: More -> More -> More # sconcat :: NonEmpty More -> More # stimes :: Integral b => b -> More -> More #
Semigroup ShortText
Instance details Defined in Data.Text.Short.Internal Methods (<>) :: ShortText -> ShortText -> ShortText # sconcat :: NonEmpty ShortText -> ShortText # stimes :: Integral b => b -> ShortText -> ShortText #
Semigroup ()	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: () -> () -> () # sconcat :: NonEmpty () -> () # stimes :: Integral b => b -> () -> () #
Semigroup (DelayedMerge hl) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise 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 Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion #
Semigroup (UnderAddition Modality) Source #	Pointwise addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality #
Semigroup (UnderAddition Quantity) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity #
Semigroup (UnderAddition Relevance) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance #
Semigroup (UnderComposition Cohesion) Source #	`Cohesion` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion #
Semigroup (UnderComposition Erased) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased #
Semigroup (UnderComposition Modality) Source #	Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality #
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 Methods (<>) :: UnderComposition Quantity -> UnderComposition Quantity -> UnderComposition Quantity # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity #
Semigroup (UnderComposition Relevance) Source #	`Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance #
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 #
Semigroup a => Semigroup (Range' a) Source #
Instance details Defined in Agda.Syntax.Position Methods (<>) :: Range' a -> Range' a -> Range' a # sconcat :: NonEmpty (Range' a) -> Range' a # stimes :: Integral b => b -> Range' a -> Range' a #
Semigroup (CallGraph cinfo) Source #	`CallGraph` is a monoid under `union`.
Instance details Defined in Agda.Termination.CallGraph Methods (<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo # sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo # stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo #
Semigroup (CMSet cinfo) Source #
Instance details Defined in Agda.Termination.CallMatrix Methods (<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo # sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo # stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo #
Semigroup m => Semigroup (TerM m) Source #
Instance details Defined in Agda.Termination.Monad Methods (<>) :: TerM m -> TerM m -> TerM m # sconcat :: NonEmpty (TerM m) -> TerM m # stimes :: Integral b => b -> TerM m -> TerM m #
Semigroup m => Semigroup (Case m) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: Case m -> Case m -> Case m # sconcat :: NonEmpty (Case m) -> Case m # stimes :: Integral b => b -> Case m -> Case m #
Semigroup c => Semigroup (WithArity c) Source #
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: WithArity c -> WithArity c -> WithArity c # sconcat :: NonEmpty (WithArity c) -> WithArity c # stimes :: Integral b => b -> WithArity c -> WithArity c #
Semigroup a => Semigroup (VarMap' a) Source #	Proper monoid instance for `VarMap` rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using `mappend`.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: VarMap' a -> VarMap' a -> VarMap' a # sconcat :: NonEmpty (VarMap' a) -> VarMap' a # stimes :: Integral b => b -> VarMap' a -> VarMap' a #
Semigroup a => Semigroup (VarOcc' a) Source #	The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair `(t₁,t₂)` then and `t₁` has `o₁` the occurrences of a variable `x` and `t₂` has `o₂` the occurrences of the same variable, then `(t₁,t₂)` has `mappend o₁ o₂` occurrences of that variable. From counting `Quantity`, we extrapolate this to `FlexRig` and `Relevance`: we care most about about `StronglyRigid` `Relevant` occurrences. E.g., if `t₁` has a `StronglyRigid` occurrence and `t₂` a `Flexible` occurrence, then `(t₁,t₂)` still has a `StronglyRigid` occurrence. Analogously, `Relevant` occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant. `VarOcc'` forms a semiring, and this monoid is the addition of the semiring.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: VarOcc' a -> VarOcc' a -> VarOcc' a # sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a # stimes :: Integral b => b -> VarOcc' a -> VarOcc' a #
Semigroup (TCM Doc) Source #	This instance is more specific than a generic instance `Semigroup a => Semigroup (TCM a)`.
Instance details Defined in Agda.TypeChecking.Pretty Methods (<>) :: TCM Doc -> TCM Doc -> TCM Doc # sconcat :: NonEmpty (TCM Doc) -> TCM Doc # stimes :: Integral b => b -> TCM Doc -> TCM Doc #
Semigroup (Match a) Source #
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods (<>) :: Match a -> Match a -> Match a # sconcat :: NonEmpty (Match a) -> Match a # stimes :: Integral b => b -> Match a -> Match a #
Ord a => Semigroup (Bag a) Source #
Instance details Defined in Agda.Utils.Bag Methods (<>) :: Bag a -> Bag a -> Bag a # sconcat :: NonEmpty (Bag a) -> Bag a # stimes :: Integral b => b -> Bag a -> Bag a #
PartialOrd a => Semigroup (Favorites a) Source #	`Favorites` forms a `Monoid` under `empty` and 'union.
Instance details Defined in Agda.Utils.Favorites Methods (<>) :: Favorites a -> Favorites a -> Favorites a # sconcat :: NonEmpty (Favorites a) -> Favorites a # stimes :: Integral b => b -> Favorites a -> Favorites a #
Semigroup a => Semigroup (RangeMap a) Source #	Merges `RangeMap`s by inserting every "piece" of the smaller one into the larger one.
Instance details Defined in Agda.Utils.RangeMap Methods (<>) :: RangeMap a -> RangeMap a -> RangeMap a # sconcat :: NonEmpty (RangeMap a) -> RangeMap a # stimes :: Integral b => b -> RangeMap a -> RangeMap a #
Bits a => Semigroup (And a)	Since: base-4.16
Instance details Defined in Data.Bits Methods (<>) :: And a -> And a -> And a # sconcat :: NonEmpty (And a) -> And a # stimes :: Integral b => b -> And a -> And a #
FiniteBits a => Semigroup (Iff a)	This constraint is arguably too strong. However, as some types (such as `Natural`) have undefined `complement`, this is the only safe choice. Since: base-4.16
Instance details Defined in Data.Bits Methods (<>) :: Iff a -> Iff a -> Iff a # sconcat :: NonEmpty (Iff a) -> Iff a # stimes :: Integral b => b -> Iff a -> Iff a #
Bits a => Semigroup (Ior a)	Since: base-4.16
Instance details Defined in Data.Bits Methods (<>) :: Ior a -> Ior a -> Ior a # sconcat :: NonEmpty (Ior a) -> Ior a # stimes :: Integral b => b -> Ior a -> Ior a #
Bits a => Semigroup (Xor a)	Since: base-4.16
Instance details Defined in Data.Bits Methods (<>) :: Xor a -> Xor a -> Xor a # sconcat :: NonEmpty (Xor a) -> Xor a # stimes :: Integral b => b -> Xor a -> Xor a #
Semigroup a => Semigroup (Identity a)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Identity Methods (<>) :: Identity a -> Identity a -> Identity a # sconcat :: NonEmpty (Identity a) -> Identity a # stimes :: Integral b => b -> Identity a -> Identity a #
Ord a => Semigroup (Max a)	Since: base-4.11.0.0
Instance details Defined in Data.Functor.Utils Methods (<>) :: Max a -> Max a -> Max a # sconcat :: NonEmpty (Max a) -> Max a # stimes :: Integral b => b -> Max a -> Max a #
Ord a => Semigroup (Min a)	Since: base-4.11.0.0
Instance details Defined in Data.Functor.Utils Methods (<>) :: Min a -> Min a -> Min a # sconcat :: NonEmpty (Min a) -> Min a # stimes :: Integral b => b -> Min a -> Min a #
Semigroup (First a)	Since: base-4.9.0.0
Instance details Defined in Data.Monoid Methods (<>) :: First a -> First a -> First a # sconcat :: NonEmpty (First a) -> First a # stimes :: Integral b => b -> First a -> First a #
Semigroup (Last a)	Since: base-4.9.0.0
Instance details Defined in Data.Monoid Methods (<>) :: Last a -> Last a -> Last a # sconcat :: NonEmpty (Last a) -> Last a # stimes :: Integral b => b -> Last a -> Last a #
Semigroup a => Semigroup (Down a)	Since: base-4.11.0.0
Instance details Defined in Data.Ord Methods (<>) :: Down a -> Down a -> Down a # sconcat :: NonEmpty (Down a) -> Down a # stimes :: Integral b => b -> Down a -> Down a #
Semigroup (First a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: First a -> First a -> First a # sconcat :: NonEmpty (First a) -> First a # stimes :: Integral b => b -> First a -> First a #
Semigroup (Last a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Last a -> Last a -> Last a # sconcat :: NonEmpty (Last a) -> Last a # stimes :: Integral b => b -> Last a -> Last a #
Ord a => Semigroup (Max a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Max a -> Max a -> Max a # sconcat :: NonEmpty (Max a) -> Max a # stimes :: Integral b => b -> Max a -> Max a #
Ord a => Semigroup (Min a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Min a -> Min a -> Min a # sconcat :: NonEmpty (Min a) -> Min a # stimes :: Integral b => b -> Min a -> Min a #
Monoid m => Semigroup (WrappedMonoid m)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup 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)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Dual a -> Dual a -> Dual a # sconcat :: NonEmpty (Dual a) -> Dual a # stimes :: Integral b => b -> Dual a -> Dual a #
Semigroup (Endo a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Endo a -> Endo a -> Endo a # sconcat :: NonEmpty (Endo a) -> Endo a # stimes :: Integral b => b -> Endo a -> Endo a #
Num a => Semigroup (Product a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Product a -> Product a -> Product a # sconcat :: NonEmpty (Product a) -> Product a # stimes :: Integral b => b -> Product a -> Product a #
Num a => Semigroup (Sum a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Sum a -> Sum a -> Sum a # sconcat :: NonEmpty (Sum a) -> Sum a # stimes :: Integral b => b -> Sum a -> Sum a #
Semigroup p => Semigroup (Par1 p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: Par1 p -> Par1 p -> Par1 p # sconcat :: NonEmpty (Par1 p) -> Par1 p # stimes :: Integral b => b -> Par1 p -> Par1 p #
Semigroup (PutM ())
Instance details Defined in Data.Binary.Put Methods (<>) :: PutM () -> PutM () -> PutM () # sconcat :: NonEmpty (PutM ()) -> PutM () # stimes :: Integral b => b -> PutM () -> PutM () #
Monoid a => Semigroup (MarkupM a)
Instance details Defined in Text.Blaze.Internal Methods (<>) :: MarkupM a -> MarkupM a -> MarkupM a # sconcat :: NonEmpty (MarkupM a) -> MarkupM a # stimes :: Integral b => b -> MarkupM a -> MarkupM a #
Semigroup (IntMap a)	Since: containers-0.5.7
Instance details Defined in Data.IntMap.Internal Methods (<>) :: IntMap a -> IntMap a -> IntMap a # sconcat :: NonEmpty (IntMap a) -> IntMap a # stimes :: Integral b => b -> IntMap a -> IntMap a #
Semigroup (Seq a)	Since: containers-0.5.7
Instance details Defined in Data.Sequence.Internal Methods (<>) :: Seq a -> Seq a -> Seq a # sconcat :: NonEmpty (Seq a) -> Seq a # stimes :: Integral b => b -> Seq a -> Seq a #
Semigroup (MergeSet a)
Instance details Defined in Data.Set.Internal Methods (<>) :: MergeSet a -> MergeSet a -> MergeSet a # sconcat :: NonEmpty (MergeSet a) -> MergeSet a # stimes :: Integral b => b -> MergeSet a -> MergeSet a #
Ord a => Semigroup (Set a)	Since: containers-0.5.7
Instance details Defined in Data.Set.Internal Methods (<>) :: Set a -> Set a -> Set a # sconcat :: NonEmpty (Set a) -> Set a # stimes :: Integral b => b -> Set a -> Set a #
Semigroup s => Semigroup (CI s)
Instance details Defined in Data.CaseInsensitive.Internal Methods (<>) :: CI s -> CI s -> CI s # sconcat :: NonEmpty (CI s) -> CI s # stimes :: Integral b => b -> CI s -> CI s #
Semigroup (DNonEmpty a)
Instance details Defined in Data.DList.DNonEmpty.Internal Methods (<>) :: DNonEmpty a -> DNonEmpty a -> DNonEmpty a # sconcat :: NonEmpty (DNonEmpty a) -> DNonEmpty a # stimes :: Integral b => b -> DNonEmpty a -> DNonEmpty a #
Semigroup (DList a)
Instance details Defined in Data.DList.Internal Methods (<>) :: DList a -> DList a -> DList a # sconcat :: NonEmpty (DList a) -> DList a # stimes :: Integral b => b -> DList a -> DList a #
Semigroup a => Semigroup (IO a)	Since: base-4.10.0.0
Instance details Defined in GHC.Base Methods (<>) :: IO a -> IO a -> IO a # sconcat :: NonEmpty (IO a) -> IO a # stimes :: Integral b => b -> IO a -> IO a #
(Hashable a, Eq a) => Semigroup (HashSet a)
Instance details Defined in Data.HashSet.Internal Methods (<>) :: HashSet a -> HashSet a -> HashSet a # sconcat :: NonEmpty (HashSet a) -> HashSet a # stimes :: Integral b => b -> HashSet a -> HashSet a #
Semigroup (Doc a)
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (<>) :: Doc a -> Doc a -> Doc a # sconcat :: NonEmpty (Doc a) -> Doc a # stimes :: Integral b => b -> Doc a -> Doc a #
Semigroup (Array a)
Instance details Defined in Data.Primitive.Array Methods (<>) :: Array a -> Array a -> Array a # sconcat :: NonEmpty (Array a) -> Array a # stimes :: Integral b => b -> Array a -> Array a #
Semigroup (PrimArray a)
Instance details Defined in Data.Primitive.PrimArray Methods (<>) :: PrimArray a -> PrimArray a -> PrimArray a # sconcat :: NonEmpty (PrimArray a) -> PrimArray a # stimes :: Integral b => b -> PrimArray a -> PrimArray a #
Semigroup (SmallArray a)
Instance details Defined in Data.Primitive.SmallArray Methods (<>) :: SmallArray a -> SmallArray a -> SmallArray a # sconcat :: NonEmpty (SmallArray a) -> SmallArray a # stimes :: Integral b => b -> SmallArray a -> SmallArray a #
Semigroup (KeyMap v)
Instance details Defined in Data.Aeson.KeyMap Methods (<>) :: KeyMap v -> KeyMap v -> KeyMap v # sconcat :: NonEmpty (KeyMap v) -> KeyMap v # stimes :: Integral b => b -> KeyMap v -> KeyMap v #
Semigroup (IResult a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: IResult a -> IResult a -> IResult a # sconcat :: NonEmpty (IResult a) -> IResult a # stimes :: Integral b => b -> IResult a -> IResult a #
Semigroup (Parser a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Parser a -> Parser a -> Parser a # sconcat :: NonEmpty (Parser a) -> Parser a # stimes :: Integral b => b -> Parser a -> Parser a #
Semigroup (Result a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Result a -> Result a -> Result a # sconcat :: NonEmpty (Result a) -> Result a # stimes :: Integral b => b -> Result a -> Result a #
Semigroup a => Semigroup (Maybe a)
Instance details Defined in Data.Strict.Maybe Methods (<>) :: Maybe a -> Maybe a -> Maybe a # sconcat :: NonEmpty (Maybe a) -> Maybe a # stimes :: Integral b => b -> Maybe a -> Maybe a #
Semigroup a => Semigroup (Concurrently a)
Instance details Defined in Control.Concurrent.Async Methods (<>) :: Concurrently a -> Concurrently a -> Concurrently a # sconcat :: NonEmpty (Concurrently a) -> Concurrently a # stimes :: Integral b => b -> Concurrently a -> Concurrently a #
Semigroup a => Semigroup (Q a)	Since: template-haskell-2.17.0.0
Instance details Defined in Language.Haskell.TH.Syntax Methods (<>) :: Q a -> Q a -> Q a # sconcat :: NonEmpty (Q a) -> Q a # stimes :: Integral b => b -> Q a -> Q a #
Semigroup (Vector a)
Instance details Defined in Data.Vector Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a # stimes :: Integral b => b -> Vector a -> Vector a #
Prim a => Semigroup (Vector a)
Instance details Defined in Data.Vector.Primitive Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a # stimes :: Integral b => b -> Vector a -> Vector a #
Storable a => Semigroup (Vector a)
Instance details Defined in Data.Vector.Storable Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a # stimes :: Integral b => b -> Vector a -> Vector a #
Semigroup (NonEmpty a)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: NonEmpty a -> NonEmpty a -> NonEmpty a # sconcat :: NonEmpty (NonEmpty a) -> NonEmpty a # stimes :: Integral b => b -> NonEmpty a -> NonEmpty a #
Semigroup a => Semigroup (Maybe a)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: Maybe a -> Maybe a -> Maybe a # sconcat :: NonEmpty (Maybe a) -> Maybe a # stimes :: Integral b => b -> Maybe a -> Maybe a #
Semigroup a => Semigroup (a)	Since: base-4.15
Instance details Defined in GHC.Base Methods (<>) :: (a) -> (a) -> (a) # sconcat :: NonEmpty (a) -> (a) # stimes :: Integral b => b -> (a) -> (a) #
Semigroup [a]	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: [a] -> [a] -> [a] # sconcat :: NonEmpty [a] -> [a] # stimes :: Integral b => b -> [a] -> [a] #
(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m # stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m #
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 Methods (<>) :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a # sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a # stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a #
(MonadIO m, Semigroup a) => Semigroup (TCMT m a) Source #	Strict (non-shortcut) semigroup. Note that there might be a lazy alternative, e.g., for TCM All we might want `and2M` as concatenation, to shortcut conjunction in case we already have `False`.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: TCMT m a -> TCMT m a -> TCMT m a # sconcat :: NonEmpty (TCMT m a) -> TCMT m a # stimes :: Integral b => b -> TCMT m a -> TCMT m a #
Monad m => Semigroup (ListT m a) Source #
Instance details Defined in Agda.Utils.ListT Methods (<>) :: ListT m a -> ListT m a -> ListT m a # sconcat :: NonEmpty (ListT m a) -> ListT m a # stimes :: Integral b => b -> ListT m a -> ListT m a #
Semigroup (Either a b)	Since: base-4.9.0.0
Instance details Defined in Data.Either Methods (<>) :: Either a b -> Either a b -> Either a b # sconcat :: NonEmpty (Either a b) -> Either a b # stimes :: Integral b0 => b0 -> Either a b -> Either a b #
Semigroup (Proxy s)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s # sconcat :: NonEmpty (Proxy s) -> Proxy s # stimes :: Integral b => b -> Proxy s -> Proxy s #
Semigroup (U1 p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: U1 p -> U1 p -> U1 p # sconcat :: NonEmpty (U1 p) -> U1 p # stimes :: Integral b => b -> U1 p -> U1 p #
Semigroup (V1 p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: V1 p -> V1 p -> V1 p # sconcat :: NonEmpty (V1 p) -> V1 p # stimes :: Integral b => b -> V1 p -> V1 p #
Semigroup a => Semigroup (ST s a)	Since: base-4.11.0.0
Instance details Defined in GHC.ST Methods (<>) :: ST s a -> ST s a -> ST s a # sconcat :: NonEmpty (ST s a) -> ST s a # stimes :: Integral b => b -> ST s a -> ST s a #
Ord k => Semigroup (Map k v)
Instance details Defined in Data.Map.Internal Methods (<>) :: Map k v -> Map k v -> Map k v # sconcat :: NonEmpty (Map k v) -> Map k v # stimes :: Integral b => b -> Map k v -> Map k v #
(Eq k, Hashable k) => Semigroup (HashMap k v)
Instance details Defined in Data.HashMap.Internal Methods (<>) :: HashMap k v -> HashMap k v -> HashMap k v # sconcat :: NonEmpty (HashMap k v) -> HashMap k v # stimes :: Integral b => b -> HashMap k v -> HashMap k v #
Semigroup (Either a b)
Instance details Defined in Data.Strict.Either Methods (<>) :: Either a b -> Either a b -> Either a b # sconcat :: NonEmpty (Either a b) -> Either a b # stimes :: Integral b0 => b0 -> Either a b -> Either a b #
(Semigroup a, Semigroup b) => Semigroup (These a b)
Instance details Defined in Data.Strict.These Methods (<>) :: These a b -> These a b -> These a b # sconcat :: NonEmpty (These a b) -> These a b # stimes :: Integral b0 => b0 -> These a b -> These a b #
(Semigroup a, Semigroup b) => Semigroup (Pair a b)
Instance details Defined in Data.Strict.Tuple Methods (<>) :: Pair a b -> Pair a b -> Pair a b # sconcat :: NonEmpty (Pair a b) -> Pair a b # stimes :: Integral b0 => b0 -> Pair a b -> Pair a b #
(Semigroup a, Semigroup b) => Semigroup (These a b)
Instance details Defined in Data.These Methods (<>) :: These a b -> These a b -> These a b # sconcat :: NonEmpty (These a b) -> These a b # stimes :: Integral b0 => b0 -> These a b -> These a b #
Semigroup (Parser i a)
Instance details Defined in Data.Attoparsec.Internal.Types Methods (<>) :: Parser i a -> Parser i a -> Parser i a # sconcat :: NonEmpty (Parser i a) -> Parser i a # stimes :: Integral b => b -> Parser i a -> Parser i a #
Semigroup b => Semigroup (a -> b)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a -> b) -> (a -> b) -> a -> b # sconcat :: NonEmpty (a -> b) -> a -> b # stimes :: Integral b0 => b0 -> (a -> b) -> a -> b #
(Semigroup a, Semigroup b) => Semigroup (a, b)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a, b) -> (a, b) -> (a, b) # sconcat :: NonEmpty (a, b) -> (a, b) # stimes :: Integral b0 => b0 -> (a, b) -> (a, b) #
Semigroup a => Semigroup (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (<>) :: Const a b -> Const a b -> Const a b # sconcat :: NonEmpty (Const a b) -> Const a b # stimes :: Integral b0 => b0 -> Const a b -> Const a b #
(Applicative f, Semigroup a) => Semigroup (Ap f a)	Since: base-4.12.0.0
Instance details Defined in Data.Monoid Methods (<>) :: Ap f a -> Ap f a -> Ap f a # sconcat :: NonEmpty (Ap f a) -> Ap f a # stimes :: Integral b => b -> Ap f a -> Ap f a #
Alternative f => Semigroup (Alt f a)	Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Alt f a -> Alt f a -> Alt f a # sconcat :: NonEmpty (Alt f a) -> Alt f a # stimes :: Integral b => b -> Alt f a -> Alt f a #
Semigroup (f p) => Semigroup (Rec1 f p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: Rec1 f p -> Rec1 f p -> Rec1 f p # sconcat :: NonEmpty (Rec1 f p) -> Rec1 f p # stimes :: Integral b => b -> Rec1 f p -> Rec1 f p #
Semigroup a => Semigroup (Tagged s a)
Instance details Defined in Data.Tagged Methods (<>) :: Tagged s a -> Tagged s a -> Tagged s a # sconcat :: NonEmpty (Tagged s a) -> Tagged s a # stimes :: Integral b => b -> Tagged s a -> Tagged s a #
(Applicative m, Semigroup doc) => Semigroup (ReaderT s m doc) Source #
Instance details Defined in Agda.Utils.Semigroup Methods (<>) :: ReaderT s m doc -> ReaderT s m doc -> ReaderT s m doc # sconcat :: NonEmpty (ReaderT s m doc) -> ReaderT s m doc # stimes :: Integral b => b -> ReaderT s m doc -> ReaderT s m doc #
(Monad m, Semigroup doc) => Semigroup (StateT s m doc) Source #
Instance details Defined in Agda.Utils.Semigroup Methods (<>) :: StateT s m doc -> StateT s m doc -> StateT s m doc # sconcat :: NonEmpty (StateT s m doc) -> StateT s m doc # stimes :: Integral b => b -> StateT s m doc -> StateT s m doc #
(Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c) -> (a, b, c) -> (a, b, c) # sconcat :: NonEmpty (a, b, c) -> (a, b, c) # stimes :: Integral b0 => b0 -> (a, b, c) -> (a, b, c) #
(Semigroup (f a), Semigroup (g a)) => Semigroup (Product f g a)	Since: base-4.16.0.0
Instance details Defined in Data.Functor.Product Methods (<>) :: Product f g a -> Product f g a -> Product f g a # sconcat :: NonEmpty (Product f g a) -> Product f g a # stimes :: Integral b => b -> Product f g a -> Product f g a #
(Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: (f :: g) p -> (f :: g) p -> (f :: g) p # sconcat :: NonEmpty ((f :: g) p) -> (f :: g) p # stimes :: Integral b => b -> (f :: g) p -> (f :*: g) p #
Semigroup c => Semigroup (K1 i c p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: K1 i c p -> K1 i c p -> K1 i c p # sconcat :: NonEmpty (K1 i c p) -> K1 i c p # stimes :: Integral b => b -> K1 i c p -> K1 i c p #
(Semigroup a, Semigroup b, Semigroup c, Semigroup d) => Semigroup (a, b, c, d)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) # sconcat :: NonEmpty (a, b, c, d) -> (a, b, c, d) # stimes :: Integral b0 => b0 -> (a, b, c, d) -> (a, b, c, d) #
Semigroup (f (g a)) => Semigroup (Compose f g a)	Since: base-4.16.0.0
Instance details Defined in Data.Functor.Compose Methods (<>) :: Compose f g a -> Compose f g a -> Compose f g a # sconcat :: NonEmpty (Compose f g a) -> Compose f g a # stimes :: Integral b => b -> Compose f g a -> Compose f g a #
Semigroup (f (g p)) => Semigroup ((f :.: g) p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: (f :.: g) p -> (f :.: g) p -> (f :.: g) p # sconcat :: NonEmpty ((f :.: g) p) -> (f :.: g) p # stimes :: Integral b => b -> (f :.: g) p -> (f :.: g) p #
Semigroup (f p) => Semigroup (M1 i c f p)	Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: M1 i c f p -> M1 i c f p -> M1 i c f p # sconcat :: NonEmpty (M1 i c f p) -> M1 i c f p # stimes :: Integral b => b -> M1 i c f p -> M1 i c f p #
(Semigroup a, Semigroup b, Semigroup c, Semigroup d, Semigroup e) => Semigroup (a, b, c, d, e)	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) # sconcat :: NonEmpty (a, b, c, d, e) -> (a, b, c, d, e) # stimes :: Integral b0 => b0 -> (a, b, c, d, e) -> (a, b, c, d, e) #

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

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

Orphan instances

Semigroup (TCM Doc) Source #	This instance is more specific than a generic instance `Semigroup a => Semigroup (TCM a)`.
Instance details Methods (<>) :: TCM Doc -> TCM Doc -> TCM Doc # sconcat :: NonEmpty (TCM Doc) -> TCM Doc # stimes :: Integral b => b -> TCM Doc -> TCM Doc #