Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Pretty

Contents

Orphan instances

Synopsis

class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> m Doc
type Doc = Doc
type MonadPretty m = MonadAbsToCon m
newtype PrettyContext = PrettyContext Context
data WithNode n a = WithNode n a
class PrettyTCMWithNode a where
- prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
pretty :: (Applicative m, Pretty a) => a -> m Doc
text :: Applicative m => String -> m Doc
prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> 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
hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
parens :: Functor m => m Doc -> m Doc
brackets :: Functor m => m Doc -> m Doc
braces :: Functor m => m Doc -> m Doc
quotes :: Functor m => m Doc -> m Doc
doubleQuotes :: Functor m => m Doc -> m Doc
comma :: Applicative m => m Doc
colon :: Applicative m => m Doc
equals :: Applicative m => m Doc
dbraces :: Functor m => m Doc -> m Doc
(<+>) :: Applicative m => m Doc -> m Doc -> m Doc
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
($$) :: Applicative m => m Doc -> m Doc -> m Doc
($+$) :: Applicative m => m Doc -> m Doc -> m Doc
pshow :: (Applicative m, Show a) => a -> m Doc
nest :: Functor m => Int -> m Doc -> m Doc
hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
prettyList :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
pwords :: Applicative m => String -> [m Doc]
fwords :: Applicative m => String -> m Doc
parensNonEmpty :: Functor m => m Doc -> m Doc
multiLineText :: Applicative m => String -> m Doc
(<?>) :: Applicative m => m Doc -> m Doc -> m Doc
prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> 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 = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

Documentation

class PrettyTCM a where Source #

Methods

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

Instances

Instances details

PrettyTCM Expr Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
PrettyTCM Pattern Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Pattern -> m Doc Source #
PrettyTCM ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem 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 Erased Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Erased -> m Doc Source #
PrettyTCM MetaId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaId -> m Doc Source #
PrettyTCM Modality Source #
Instance details Defined in Agda.TypeChecking.Pretty 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 TopLevelModuleName Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TopLevelModuleName -> m Doc Source #
PrettyTCM NamedClause Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
PrettyTCM SplitPatVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods prettyTCM :: MonadPretty m => SplitPatVar -> 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 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 ContextEntry Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ContextEntry -> 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 NamedMeta Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedMeta -> 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 NoLeftInv Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => NoLeftInv -> m Doc Source #
PrettyTCM UnifyState Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyState -> m Doc Source #
PrettyTCM UnifyStep Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyStep -> 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 Flex Source #
Instance details Defined in Agda.TypeChecking.SizedTypes.Syntax Methods prettyTCM :: MonadPretty m => Flex -> m Doc Source #
PrettyTCM ErrorPart Source #
Instance details Defined in Agda.TypeChecking.Unquote 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 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 #
(Pretty a, Pretty b) => PrettyTCM (OutputForm a b) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods prettyTCM :: MonadPretty m => OutputForm a b -> m Doc Source #
(PrettyTCM n, PrettyTCMWithNode e) => PrettyTCM (Graph n e) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Graph n e -> m Doc Source #
(PrettyTCM k, PrettyTCM v) => PrettyTCM (Map k v) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Map k v -> m Doc Source #
(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => (a, b) -> m Doc Source #
(PrettyTCM a, PrettyTCM b, PrettyTCM c) => PrettyTCM (a, b, c) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => (a, b, c) -> m Doc Source #

type Doc = Doc Source #

type MonadPretty m = MonadAbsToCon m Source #

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 #

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a

class PrettyTCMWithNode a where Source #

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

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 #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

comma :: Applicative m => m Doc Source #

colon :: Applicative m => m Doc Source #

equals :: Applicative m => m Doc Source #

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

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

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

prettyList without the brackets.

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

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

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

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

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

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

Comma-separated list in brackets.

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

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

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

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

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

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

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

Pretty print with a given context precedence

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

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

Proper pretty printing of patterns:

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

class Semigroup a where #

Minimal complete definition

(<>) | sconcat

Methods

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

Instances

Instances details

Semigroup IsMain Source #	Conjunctive semigroup (`NotMain` is absorbing).
Instance details Defined in Agda.Compiler.Common Methods (<>) :: IsMain -> IsMain -> IsMain # sconcat :: NonEmpty IsMain -> IsMain stimes :: Integral b => b -> IsMain -> IsMain
Semigroup Doc Source #
Instance details Defined in Agda.Compiler.JS.Pretty Methods (<>) :: Doc -> Doc -> Doc # sconcat :: NonEmpty Doc -> Doc stimes :: Integral b => b -> Doc -> Doc
Semigroup Comment Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods (<>) :: Comment -> Comment -> Comment # sconcat :: NonEmpty Comment -> Comment stimes :: Integral b => b -> Comment -> Comment
Semigroup HsCompileState Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc 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 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 OptionsPragma Source #
Instance details Defined in Agda.Interaction.Library.Base Methods (<>) :: OptionsPragma -> OptionsPragma -> OptionsPragma # sconcat :: NonEmpty OptionsPragma -> OptionsPragma stimes :: Integral b => b -> OptionsPragma -> OptionsPragma
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 JointOpacity Source #
Instance details Defined in Agda.Syntax.Common Methods (<>) :: JointOpacity -> JointOpacity -> JointOpacity # sconcat :: NonEmpty JointOpacity -> JointOpacity stimes :: Integral b => b -> JointOpacity -> JointOpacity
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 Aspect Source #	`NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: Aspect -> Aspect -> Aspect # sconcat :: NonEmpty Aspect -> Aspect stimes :: Integral b => b -> Aspect -> Aspect
Semigroup Aspects Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspects -> Aspects -> Aspects # sconcat :: NonEmpty Aspects -> Aspects stimes :: Integral b => b -> Aspects -> Aspects
Semigroup DefinitionSite Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise 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.Syntax.Common.Aspect Methods (<>) :: NameKind -> NameKind -> NameKind # sconcat :: NonEmpty NameKind -> NameKind stimes :: Integral b => b -> NameKind -> NameKind
Semigroup TokenBased Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased # sconcat :: NonEmpty TokenBased -> TokenBased stimes :: Integral b => b -> TokenBased -> TokenBased
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 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 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 UnifyOutput Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods (<>) :: UnifyOutput -> UnifyOutput -> UnifyOutput # sconcat :: NonEmpty UnifyOutput -> UnifyOutput stimes :: Integral b => b -> UnifyOutput -> UnifyOutput
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 ByteArray
Instance details Defined in Data.Array.Byte Methods (<>) :: ByteArray -> ByteArray -> ByteArray # sconcat :: NonEmpty ByteArray -> ByteArray stimes :: Integral b => b -> ByteArray -> ByteArray
Semigroup All
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: All -> All -> All # sconcat :: NonEmpty All -> All stimes :: Integral b => b -> All -> All
Semigroup Any
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Any -> Any -> Any # sconcat :: NonEmpty Any -> Any stimes :: Integral b => b -> Any -> Any
Semigroup Void
Instance details Defined in GHC.Base Methods (<>) :: Void -> Void -> Void # sconcat :: NonEmpty Void -> Void stimes :: Integral b => b -> Void -> Void
Semigroup Attribute
Instance details Defined in Text.Blaze.Internal Methods (<>) :: Attribute -> Attribute -> Attribute # sconcat :: NonEmpty Attribute -> Attribute stimes :: Integral b => b -> Attribute -> Attribute
Semigroup AttributeValue
Instance details Defined in Text.Blaze.Internal Methods (<>) :: AttributeValue -> AttributeValue -> AttributeValue # sconcat :: NonEmpty AttributeValue -> AttributeValue stimes :: Integral b => b -> AttributeValue -> AttributeValue
Semigroup ChoiceString
Instance details Defined in Text.Blaze.Internal Methods (<>) :: ChoiceString -> ChoiceString -> ChoiceString # sconcat :: NonEmpty ChoiceString -> ChoiceString stimes :: Integral b => b -> ChoiceString -> ChoiceString
Semigroup Builder
Instance details Defined in Data.ByteString.Builder.Internal Methods (<>) :: Builder -> Builder -> Builder # sconcat :: NonEmpty Builder -> Builder stimes :: Integral b => b -> Builder -> Builder
Semigroup ByteString
Instance details Defined in Data.ByteString.Internal.Type Methods (<>) :: ByteString -> ByteString -> ByteString # sconcat :: NonEmpty ByteString -> ByteString stimes :: Integral b => b -> ByteString -> ByteString
Semigroup ByteString
Instance details Defined in Data.ByteString.Lazy.Internal Methods (<>) :: ByteString -> ByteString -> ByteString # sconcat :: NonEmpty ByteString -> ByteString stimes :: Integral b => b -> ByteString -> ByteString
Semigroup ShortByteString
Instance details Defined in Data.ByteString.Short.Internal Methods (<>) :: ShortByteString -> ShortByteString -> ShortByteString # sconcat :: NonEmpty ShortByteString -> ShortByteString stimes :: Integral b => b -> ShortByteString -> ShortByteString
Semigroup IntSet
Instance details Defined in Data.IntSet.Internal Methods (<>) :: IntSet -> IntSet -> IntSet # sconcat :: NonEmpty IntSet -> IntSet stimes :: Integral b => b -> IntSet -> IntSet
Semigroup OsString
Instance details Defined in System.OsString.Internal.Types Methods (<>) :: OsString -> OsString -> OsString # sconcat :: NonEmpty OsString -> OsString stimes :: Integral b => b -> OsString -> OsString
Semigroup PosixString
Instance details Defined in System.OsString.Internal.Types Methods (<>) :: PosixString -> PosixString -> PosixString # sconcat :: NonEmpty PosixString -> PosixString stimes :: Integral b => b -> PosixString -> PosixString
Semigroup WindowsString
Instance details Defined in System.OsString.Internal.Types Methods (<>) :: WindowsString -> WindowsString -> WindowsString # sconcat :: NonEmpty WindowsString -> WindowsString stimes :: Integral b => b -> WindowsString -> WindowsString
Semigroup Ordering
Instance details Defined in GHC.Base Methods (<>) :: Ordering -> Ordering -> Ordering # sconcat :: NonEmpty Ordering -> Ordering stimes :: Integral b => b -> Ordering -> Ordering
Semigroup Doc
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (<>) :: Doc -> Doc -> Doc # sconcat :: NonEmpty Doc -> Doc stimes :: Integral b => b -> Doc -> Doc
Semigroup Series
Instance details Defined in Data.Aeson.Encoding.Internal Methods (<>) :: Series -> Series -> Series # sconcat :: NonEmpty Series -> Series stimes :: Integral b => b -> Series -> Series
Semigroup Key
Instance details Defined in Data.Aeson.Key Methods (<>) :: Key -> Key -> Key # sconcat :: NonEmpty Key -> Key stimes :: Integral b => b -> Key -> Key
Semigroup ShortText
Instance details Defined in Data.Text.Short.Internal Methods (<>) :: ShortText -> ShortText -> ShortText # sconcat :: NonEmpty ShortText -> ShortText stimes :: Integral b => b -> ShortText -> ShortText
Semigroup ()
Instance details Defined in GHC.Base Methods (<>) :: () -> () -> () # sconcat :: NonEmpty () -> () stimes :: Integral b => b -> () -> ()
Semigroup (DelayedMerge hl) Source #
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl # sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl
Semigroup (UnderAddition Cohesion) Source #	`Cohesion` forms a semigroup under addition.
Instance details Defined in Agda.Syntax.Common 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
Eq a => Semigroup (Range' a) Source #
Instance details Defined in Agda.Syntax.Position Methods (<>) :: Range' a -> Range' a -> Range' a # sconcat :: NonEmpty (Range' a) -> Range' a stimes :: Integral b => b -> Range' a -> Range' a
Semigroup (AbsToCon Doc) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods (<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc # sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc
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
SmallSetElement a => Semigroup (SmallSet a) Source #
Instance details Defined in Agda.Utils.SmallSet Methods (<>) :: SmallSet a -> SmallSet a -> SmallSet a # sconcat :: NonEmpty (SmallSet a) -> SmallSet a stimes :: Integral b => b -> SmallSet a -> SmallSet a
Bits a => Semigroup (And a)
Instance details Defined in Data.Bits Methods (<>) :: And a -> And a -> And a # sconcat :: NonEmpty (And a) -> And a stimes :: Integral b => b -> And a -> And a
FiniteBits a => Semigroup (Iff a)
Instance details Defined in Data.Bits Methods (<>) :: Iff a -> Iff a -> Iff a # sconcat :: NonEmpty (Iff a) -> Iff a stimes :: Integral b => b -> Iff a -> Iff a
Bits a => Semigroup (Ior a)
Instance details Defined in Data.Bits Methods (<>) :: Ior a -> Ior a -> Ior a # sconcat :: NonEmpty (Ior a) -> Ior a stimes :: Integral b => b -> Ior a -> Ior a
Bits a => Semigroup (Xor a)
Instance details Defined in Data.Bits Methods (<>) :: Xor a -> Xor a -> Xor a # sconcat :: NonEmpty (Xor a) -> Xor a stimes :: Integral b => b -> Xor a -> Xor a
Semigroup a => Semigroup (Identity a)
Instance details Defined in Data.Functor.Identity Methods (<>) :: Identity a -> Identity a -> Identity a # sconcat :: NonEmpty (Identity a) -> Identity a stimes :: Integral b => b -> Identity a -> Identity a
Semigroup (First a)
Instance details Defined in Data.Monoid Methods (<>) :: First a -> First a -> First a # sconcat :: NonEmpty (First a) -> First a stimes :: Integral b => b -> First a -> First a
Semigroup (Last a)
Instance details Defined in Data.Monoid Methods (<>) :: Last a -> Last a -> Last a # sconcat :: NonEmpty (Last a) -> Last a stimes :: Integral b => b -> Last a -> Last a
Semigroup a => Semigroup (Down a)
Instance details Defined in Data.Ord Methods (<>) :: Down a -> Down a -> Down a # sconcat :: NonEmpty (Down a) -> Down a stimes :: Integral b => b -> Down a -> Down a
Semigroup (First a)
Instance details Defined in Data.Semigroup Methods (<>) :: First a -> First a -> First a # sconcat :: NonEmpty (First a) -> First a stimes :: Integral b => b -> First a -> First a
Semigroup (Last a)
Instance details Defined in Data.Semigroup Methods (<>) :: Last a -> Last a -> Last a # sconcat :: NonEmpty (Last a) -> Last a stimes :: Integral b => b -> Last a -> Last a
Ord a => Semigroup (Max a)
Instance details Defined in Data.Semigroup Methods (<>) :: Max a -> Max a -> Max a # sconcat :: NonEmpty (Max a) -> Max a stimes :: Integral b => b -> Max a -> Max a
Ord a => Semigroup (Min a)
Instance details Defined in Data.Semigroup Methods (<>) :: Min a -> Min a -> Min a # sconcat :: NonEmpty (Min a) -> Min a stimes :: Integral b => b -> Min a -> Min a
Monoid m => Semigroup (WrappedMonoid m)
Instance details Defined in Data.Semigroup Methods (<>) :: WrappedMonoid m -> WrappedMonoid m -> WrappedMonoid m # sconcat :: NonEmpty (WrappedMonoid m) -> WrappedMonoid m stimes :: Integral b => b -> WrappedMonoid m -> WrappedMonoid m
Semigroup a => Semigroup (Dual a)
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Dual a -> Dual a -> Dual a # sconcat :: NonEmpty (Dual a) -> Dual a stimes :: Integral b => b -> Dual a -> Dual a
Semigroup (Endo a)
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Endo a -> Endo a -> Endo a # sconcat :: NonEmpty (Endo a) -> Endo a stimes :: Integral b => b -> Endo a -> Endo a
Num a => Semigroup (Product a)
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Product a -> Product a -> Product a # sconcat :: NonEmpty (Product a) -> Product a stimes :: Integral b => b -> Product a -> Product a
Num a => Semigroup (Sum a)
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Sum a -> Sum a -> Sum a # sconcat :: NonEmpty (Sum a) -> Sum a stimes :: Integral b => b -> Sum a -> Sum a
Semigroup (NonEmpty a)
Instance details Defined in GHC.Base Methods (<>) :: NonEmpty a -> NonEmpty a -> NonEmpty a # sconcat :: NonEmpty (NonEmpty a) -> NonEmpty a stimes :: Integral b => b -> NonEmpty a -> NonEmpty a
Semigroup a => Semigroup (STM a)
Instance details Defined in GHC.Conc.Sync Methods (<>) :: STM a -> STM a -> STM a # sconcat :: NonEmpty (STM a) -> STM a stimes :: Integral b => b -> STM a -> STM a
(Generic a, Semigroup (Rep a ())) => Semigroup (Generically a)
Instance details Defined in GHC.Generics Methods (<>) :: Generically a -> Generically a -> Generically a # sconcat :: NonEmpty (Generically a) -> Generically a stimes :: Integral b => b -> Generically a -> Generically a
Semigroup p => Semigroup (Par1 p)
Instance details Defined in GHC.Generics Methods (<>) :: Par1 p -> Par1 p -> Par1 p # sconcat :: NonEmpty (Par1 p) -> Par1 p stimes :: Integral b => b -> Par1 p -> Par1 p
Semigroup (PutM ())
Instance details Defined in Data.Binary.Put Methods (<>) :: PutM () -> PutM () -> PutM () # sconcat :: NonEmpty (PutM ()) -> PutM () stimes :: Integral b => b -> PutM () -> PutM ()
Monoid a => Semigroup (MarkupM a)
Instance details Defined in Text.Blaze.Internal Methods (<>) :: MarkupM a -> MarkupM a -> MarkupM a # sconcat :: NonEmpty (MarkupM a) -> MarkupM a stimes :: Integral b => b -> MarkupM a -> MarkupM a
Num a => Semigroup (AlphaColour a)
Instance details Defined in Data.Colour.Internal Methods (<>) :: AlphaColour a -> AlphaColour a -> AlphaColour a # sconcat :: NonEmpty (AlphaColour a) -> AlphaColour a stimes :: Integral b => b -> AlphaColour a -> AlphaColour a
Num a => Semigroup (Colour a)
Instance details Defined in Data.Colour.Internal Methods (<>) :: Colour a -> Colour a -> Colour a # sconcat :: NonEmpty (Colour a) -> Colour a stimes :: Integral b => b -> Colour a -> Colour a
Semigroup (IntMap a)
Instance details Defined in Data.IntMap.Internal Methods (<>) :: IntMap a -> IntMap a -> IntMap a # sconcat :: NonEmpty (IntMap a) -> IntMap a stimes :: Integral b => b -> IntMap a -> IntMap a
Semigroup (Seq a)
Instance details Defined in Data.Sequence.Internal Methods (<>) :: Seq a -> Seq a -> Seq a # sconcat :: NonEmpty (Seq a) -> Seq a stimes :: Integral b => b -> Seq a -> Seq a
Ord a => Semigroup (Intersection a)
Instance details Defined in Data.Set.Internal Methods (<>) :: Intersection a -> Intersection a -> Intersection a # sconcat :: NonEmpty (Intersection a) -> Intersection a stimes :: Integral b => b -> Intersection a -> Intersection a
Semigroup (MergeSet a)
Instance details Defined in Data.Set.Internal Methods (<>) :: MergeSet a -> MergeSet a -> MergeSet a # sconcat :: NonEmpty (MergeSet a) -> MergeSet a stimes :: Integral b => b -> MergeSet a -> MergeSet a
Ord a => Semigroup (Set a)
Instance details Defined in Data.Set.Internal Methods (<>) :: Set a -> Set a -> Set a # sconcat :: NonEmpty (Set a) -> Set a stimes :: Integral b => b -> Set a -> Set a
Semigroup s => Semigroup (CI s)
Instance details Defined in Data.CaseInsensitive.Internal Methods (<>) :: CI s -> CI s -> CI s # sconcat :: NonEmpty (CI s) -> CI s stimes :: Integral b => b -> CI s -> CI s
Semigroup (DNonEmpty a)
Instance details Defined in Data.DList.DNonEmpty.Internal Methods (<>) :: DNonEmpty a -> DNonEmpty a -> DNonEmpty a # sconcat :: NonEmpty (DNonEmpty a) -> DNonEmpty a stimes :: Integral b => b -> DNonEmpty a -> DNonEmpty a
Semigroup (DList a)
Instance details Defined in Data.DList.Internal Methods (<>) :: DList a -> DList a -> DList a # sconcat :: NonEmpty (DList a) -> DList a stimes :: Integral b => b -> DList a -> DList a
Semigroup a => Semigroup (IO a)
Instance details Defined in GHC.Base Methods (<>) :: IO a -> IO a -> IO a # sconcat :: NonEmpty (IO a) -> IO a stimes :: Integral b => b -> IO a -> IO a
(Hashable a, Eq a) => Semigroup (HashSet a)
Instance details Defined in Data.HashSet.Internal Methods (<>) :: HashSet a -> HashSet a -> HashSet a # sconcat :: NonEmpty (HashSet a) -> HashSet a stimes :: Integral b => b -> HashSet a -> HashSet a
Semigroup (Doc a)
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (<>) :: Doc a -> Doc a -> Doc a # sconcat :: NonEmpty (Doc a) -> Doc a stimes :: Integral b => b -> Doc a -> Doc a
Semigroup (Array a)
Instance details Defined in Data.Primitive.Array Methods (<>) :: Array a -> Array a -> Array a # sconcat :: NonEmpty (Array a) -> Array a stimes :: Integral b => b -> Array a -> Array a
Semigroup (PrimArray a)
Instance details Defined in Data.Primitive.PrimArray Methods (<>) :: PrimArray a -> PrimArray a -> PrimArray a # sconcat :: NonEmpty (PrimArray a) -> PrimArray a stimes :: Integral b => b -> PrimArray a -> PrimArray a
Semigroup (SmallArray a)
Instance details Defined in Data.Primitive.SmallArray Methods (<>) :: SmallArray a -> SmallArray a -> SmallArray a # sconcat :: NonEmpty (SmallArray a) -> SmallArray a stimes :: Integral b => b -> SmallArray a -> SmallArray a
Semigroup (KeyMap v)
Instance details Defined in Data.Aeson.KeyMap Methods (<>) :: KeyMap v -> KeyMap v -> KeyMap v # sconcat :: NonEmpty (KeyMap v) -> KeyMap v stimes :: Integral b => b -> KeyMap v -> KeyMap v
Semigroup (IResult a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: IResult a -> IResult a -> IResult a # sconcat :: NonEmpty (IResult a) -> IResult a stimes :: Integral b => b -> IResult a -> IResult a
Semigroup (Parser a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Parser a -> Parser a -> Parser a # sconcat :: NonEmpty (Parser a) -> Parser a stimes :: Integral b => b -> Parser a -> Parser a
Semigroup (Result a)
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Result a -> Result a -> Result a # sconcat :: NonEmpty (Result a) -> Result a stimes :: Integral b => b -> Result a -> Result a
Semigroup a => Semigroup (Maybe a)
Instance details Defined in Data.Strict.Maybe Methods (<>) :: Maybe a -> Maybe a -> Maybe a # sconcat :: NonEmpty (Maybe a) -> Maybe a stimes :: Integral b => b -> Maybe a -> Maybe a
Semigroup a => Semigroup (Concurrently a)
Instance details Defined in Control.Concurrent.Async Methods (<>) :: Concurrently a -> Concurrently a -> Concurrently a # sconcat :: NonEmpty (Concurrently a) -> Concurrently a stimes :: Integral b => b -> Concurrently a -> Concurrently a
Semigroup a => Semigroup (Q a)
Instance details Defined in Language.Haskell.TH.Syntax Methods (<>) :: Q a -> Q a -> Q a # sconcat :: NonEmpty (Q a) -> Q a stimes :: Integral b => b -> Q a -> Q a
Semigroup (Vector a)
Instance details Defined in Data.Vector Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a stimes :: Integral b => b -> Vector a -> Vector a
Prim a => Semigroup (Vector a)
Instance details Defined in Data.Vector.Primitive Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a stimes :: Integral b => b -> Vector a -> Vector a
Storable a => Semigroup (Vector a)
Instance details Defined in Data.Vector.Storable Methods (<>) :: Vector a -> Vector a -> Vector a # sconcat :: NonEmpty (Vector a) -> Vector a stimes :: Integral b => b -> Vector a -> Vector a
Semigroup a => Semigroup (Maybe a)
Instance details Defined in GHC.Base Methods (<>) :: Maybe a -> Maybe a -> Maybe a # sconcat :: NonEmpty (Maybe a) -> Maybe a stimes :: Integral b => b -> Maybe a -> Maybe a
Semigroup a => Semigroup (a)
Instance details Defined in GHC.Base Methods (<>) :: (a) -> (a) -> (a) # sconcat :: NonEmpty (a) -> (a) stimes :: Integral b => b -> (a) -> (a)
Semigroup [a]
Instance details Defined in GHC.Base Methods (<>) :: [a] -> [a] -> [a] # sconcat :: NonEmpty [a] -> [a] stimes :: Integral b => b -> [a] -> [a]
(HasRange n, HasRange m) => Semigroup (ImportDirective' n m) Source #
Instance details Defined in Agda.Syntax.Common 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)
Instance details Defined in Data.Either Methods (<>) :: Either a b -> Either a b -> Either a b # sconcat :: NonEmpty (Either a b) -> Either a b stimes :: Integral b0 => b0 -> Either a b -> Either a b
Semigroup (Proxy s)
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s # sconcat :: NonEmpty (Proxy s) -> Proxy s stimes :: Integral b => b -> Proxy s -> Proxy s
Semigroup (U1 p)
Instance details Defined in GHC.Generics Methods (<>) :: U1 p -> U1 p -> U1 p # sconcat :: NonEmpty (U1 p) -> U1 p stimes :: Integral b => b -> U1 p -> U1 p
Semigroup (V1 p)
Instance details Defined in GHC.Generics Methods (<>) :: V1 p -> V1 p -> V1 p # sconcat :: NonEmpty (V1 p) -> V1 p stimes :: Integral b => b -> V1 p -> V1 p
Semigroup a => Semigroup (ST s a)
Instance details Defined in GHC.ST Methods (<>) :: ST s a -> ST s a -> ST s a # sconcat :: NonEmpty (ST s a) -> ST s a stimes :: Integral b => b -> ST s a -> ST s a
Ord k => Semigroup (Map k v)
Instance details Defined in Data.Map.Internal Methods (<>) :: Map k v -> Map k v -> Map k v # sconcat :: NonEmpty (Map k v) -> Map k v stimes :: Integral b => b -> Map k v -> Map k v
(Eq k, Hashable k) => Semigroup (HashMap k v)
Instance details Defined in Data.HashMap.Internal Methods (<>) :: HashMap k v -> HashMap k v -> HashMap k v # sconcat :: NonEmpty (HashMap k v) -> HashMap k v stimes :: Integral b => b -> HashMap k v -> HashMap k v
Semigroup (Either a b)
Instance details Defined in Data.Strict.Either Methods (<>) :: Either a b -> Either a b -> Either a b # sconcat :: NonEmpty (Either a b) -> Either a b stimes :: Integral b0 => b0 -> Either a b -> Either a b
(Semigroup a, Semigroup b) => Semigroup (These a b)
Instance details Defined in Data.Strict.These Methods (<>) :: These a b -> These a b -> These a b # sconcat :: NonEmpty (These a b) -> These a b stimes :: Integral b0 => b0 -> These a b -> These a b
(Semigroup a, Semigroup b) => Semigroup (Pair a b)
Instance details Defined in Data.Strict.Tuple Methods (<>) :: Pair a b -> Pair a b -> Pair a b # sconcat :: NonEmpty (Pair a b) -> Pair a b stimes :: Integral b0 => b0 -> Pair a b -> Pair a b
(Semigroup a, Semigroup b) => Semigroup (These a b)
Instance details Defined in Data.These Methods (<>) :: These a b -> These a b -> These a b # sconcat :: NonEmpty (These a b) -> These a b stimes :: Integral b0 => b0 -> These a b -> These a b
(Semigroup a, Semigroup b) => Semigroup (a, b)
Instance details Defined in GHC.Base Methods (<>) :: (a, b) -> (a, b) -> (a, b) # sconcat :: NonEmpty (a, b) -> (a, b) stimes :: Integral b0 => b0 -> (a, b) -> (a, b)
Semigroup b => Semigroup (a -> b)
Instance details Defined in GHC.Base Methods (<>) :: (a -> b) -> (a -> b) -> a -> b # sconcat :: NonEmpty (a -> b) -> a -> b stimes :: Integral b0 => b0 -> (a -> b) -> a -> b
Semigroup a => Semigroup (Const a b)
Instance details Defined in Data.Functor.Const Methods (<>) :: Const a b -> Const a b -> Const a b # sconcat :: NonEmpty (Const a b) -> Const a b stimes :: Integral b0 => b0 -> Const a b -> Const a b
(Applicative f, Semigroup a) => Semigroup (Ap f a)
Instance details Defined in Data.Monoid Methods (<>) :: Ap f a -> Ap f a -> Ap f a # sconcat :: NonEmpty (Ap f a) -> Ap f a stimes :: Integral b => b -> Ap f a -> Ap f a
Alternative f => Semigroup (Alt f a)
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Alt f a -> Alt f a -> Alt f a # sconcat :: NonEmpty (Alt f a) -> Alt f a stimes :: Integral b => b -> Alt f a -> Alt f a
Semigroup (f p) => Semigroup (Rec1 f p)
Instance details Defined in GHC.Generics Methods (<>) :: Rec1 f p -> Rec1 f p -> Rec1 f p # sconcat :: NonEmpty (Rec1 f p) -> Rec1 f p stimes :: Integral b => b -> Rec1 f p -> Rec1 f p
Semigroup a => Semigroup (Tagged s a)
Instance details Defined in Data.Tagged Methods (<>) :: Tagged s a -> Tagged s a -> Tagged s a # sconcat :: NonEmpty (Tagged s a) -> Tagged s a stimes :: Integral b => b -> Tagged s a -> Tagged s a
(Applicative m, Semigroup doc) => Semigroup (ReaderT s m doc) Source #
Instance details Defined in Agda.Utils.Semigroup Methods (<>) :: ReaderT s m doc -> ReaderT s m doc -> ReaderT s m doc # sconcat :: NonEmpty (ReaderT s m doc) -> ReaderT s m doc stimes :: Integral b => b -> ReaderT s m doc -> ReaderT s m doc
(Monad m, Semigroup doc) => Semigroup (StateT s m doc) Source #
Instance details Defined in Agda.Utils.Semigroup Methods (<>) :: StateT s m doc -> StateT s m doc -> StateT s m doc # sconcat :: NonEmpty (StateT s m doc) -> StateT s m doc stimes :: Integral b => b -> StateT s m doc -> StateT s m doc
Semigroup a => Semigroup (Constant a b)
Instance details Defined in Data.Functor.Constant Methods (<>) :: Constant a b -> Constant a b -> Constant a b # sconcat :: NonEmpty (Constant a b) -> Constant a b stimes :: Integral b0 => b0 -> Constant a b -> Constant a b
(Semigroup a, Semigroup b, Semigroup c) => Semigroup (a, b, c)
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c) -> (a, b, c) -> (a, b, c) # sconcat :: NonEmpty (a, b, c) -> (a, b, c) stimes :: Integral b0 => b0 -> (a, b, c) -> (a, b, c)
(Semigroup (f a), Semigroup (g a)) => Semigroup (Product f g a)
Instance details Defined in Data.Functor.Product Methods (<>) :: Product f g a -> Product f g a -> Product f g a # sconcat :: NonEmpty (Product f g a) -> Product f g a stimes :: Integral b => b -> Product f g a -> Product f g a
(Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p)
Instance details Defined in GHC.Generics Methods (<>) :: (f :: g) p -> (f :: g) p -> (f :: g) p # sconcat :: NonEmpty ((f :: g) p) -> (f :: g) p stimes :: Integral b => b -> (f :: g) p -> (f :*: g) p
Semigroup c => Semigroup (K1 i c p)
Instance details Defined in GHC.Generics Methods (<>) :: K1 i c p -> K1 i c p -> K1 i c p # sconcat :: NonEmpty (K1 i c p) -> K1 i c p stimes :: Integral b => b -> K1 i c p -> K1 i c p
(Semigroup a, Semigroup b, Semigroup c, Semigroup d) => Semigroup (a, b, c, d)
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) # sconcat :: NonEmpty (a, b, c, d) -> (a, b, c, d) stimes :: Integral b0 => b0 -> (a, b, c, d) -> (a, b, c, d)
Semigroup (f (g a)) => Semigroup (Compose f g a)
Instance details Defined in Data.Functor.Compose Methods (<>) :: Compose f g a -> Compose f g a -> Compose f g a # sconcat :: NonEmpty (Compose f g a) -> Compose f g a stimes :: Integral b => b -> Compose f g a -> Compose f g a
Semigroup (f (g p)) => Semigroup ((f :.: g) p)
Instance details Defined in GHC.Generics Methods (<>) :: (f :.: g) p -> (f :.: g) p -> (f :.: g) p # sconcat :: NonEmpty ((f :.: g) p) -> (f :.: g) p stimes :: Integral b => b -> (f :.: g) p -> (f :.: g) p
Semigroup (f p) => Semigroup (M1 i c f p)
Instance details Defined in GHC.Generics Methods (<>) :: M1 i c f p -> M1 i c f p -> M1 i c f p # sconcat :: NonEmpty (M1 i c f p) -> M1 i c f p stimes :: Integral b => b -> M1 i c f p -> M1 i c f p
(Semigroup a, Semigroup b, Semigroup c, Semigroup d, Semigroup e) => Semigroup (a, b, c, d, e)
Instance details Defined in GHC.Base Methods (<>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) # sconcat :: NonEmpty (a, b, c, d, e) -> (a, b, c, d, e) stimes :: Integral b0 => b0 -> (a, b, c, d, e) -> (a, b, c, d, e)

type MonadAbsToCon m = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #

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

Orphan instances

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