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

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

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

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 Source # sconcat :: NonEmpty IsMain -> IsMain Source # stimes :: Integral b => b -> IsMain -> IsMain Source #
Semigroup Doc Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods (<>) :: Doc -> Doc -> Doc Source # sconcat :: NonEmpty Doc -> Doc Source # stimes :: Integral b => b -> Doc -> Doc Source #
Semigroup Comment Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (<>) :: Comment -> Comment -> Comment Source # sconcat :: NonEmpty Comment -> Comment Source # stimes :: Integral b => b -> Comment -> Comment Source #
Semigroup UsesFloat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods (<>) :: UsesFloat -> UsesFloat -> UsesFloat Source # sconcat :: NonEmpty UsesFloat -> UsesFloat Source # stimes :: Integral b => b -> UsesFloat -> UsesFloat Source #
Semigroup HsCompileState Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState Source # sconcat :: NonEmpty HsCompileState -> HsCompileState Source # stimes :: Integral b => b -> HsCompileState -> HsCompileState Source #
Semigroup Occurs Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: Occurs -> Occurs -> Occurs Source # sconcat :: NonEmpty Occurs -> Occurs Source # stimes :: Integral b => b -> Occurs -> Occurs Source #
Semigroup SeqArg Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: SeqArg -> SeqArg -> SeqArg Source # sconcat :: NonEmpty SeqArg -> SeqArg Source # stimes :: Integral b => b -> SeqArg -> SeqArg Source #
Semigroup UnderLambda Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods (<>) :: UnderLambda -> UnderLambda -> UnderLambda Source # sconcat :: NonEmpty UnderLambda -> UnderLambda Source # stimes :: Integral b => b -> UnderLambda -> UnderLambda Source #
Semigroup Aspect Source # | `NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspect -> Aspect -> Aspect Source # sconcat :: NonEmpty Aspect -> Aspect Source # stimes :: Integral b => b -> Aspect -> Aspect Source #
Semigroup Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspects -> Aspects -> Aspects Source # sconcat :: NonEmpty Aspects -> Aspects Source # stimes :: Integral b => b -> Aspects -> Aspects Source #
Semigroup DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite Source # sconcat :: NonEmpty DefinitionSite -> DefinitionSite Source # stimes :: Integral b => b -> DefinitionSite -> DefinitionSite Source #
Semigroup NameKind Source # | Some `NameKind`s are more informative than others.
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: NameKind -> NameKind -> NameKind Source # sconcat :: NonEmpty NameKind -> NameKind Source # stimes :: Integral b => b -> NameKind -> NameKind Source #
Semigroup PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: PositionMap -> PositionMap -> PositionMap Source # sconcat :: NonEmpty PositionMap -> PositionMap Source # stimes :: Integral b => b -> PositionMap -> PositionMap Source #
Semigroup TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased Source # sconcat :: NonEmpty TokenBased -> TokenBased Source # stimes :: Integral b => b -> TokenBased -> TokenBased Source #
Semigroup CoverageCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck Source # sconcat :: NonEmpty CoverageCheck -> CoverageCheck Source # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck Source #
Semigroup ExpandedEllipsis Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis Source # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis Source # stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis Source #
Semigroup FreeVariables Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables Source # sconcat :: NonEmpty FreeVariables -> FreeVariables Source # stimes :: Integral b => b -> FreeVariables -> FreeVariables Source #
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 Source # sconcat :: NonEmpty Hiding -> Hiding Source # stimes :: Integral b => b -> Hiding -> Hiding Source #
Semigroup IsAbstract Source # | Semigroup computes if any of several is an `AbstractDef`.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract Source # sconcat :: NonEmpty IsAbstract -> IsAbstract Source # stimes :: Integral b => b -> IsAbstract -> IsAbstract Source #
Semigroup Overlappable Source # | Just for the `Hiding` instance. Should never combine different overlapping.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable Source # sconcat :: NonEmpty Overlappable -> Overlappable Source # stimes :: Integral b => b -> Overlappable -> Overlappable Source #
Semigroup PositivityCheck Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck Source # sconcat :: NonEmpty PositivityCheck -> PositivityCheck Source # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck Source #
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 Source # sconcat :: NonEmpty Q0Origin -> Q0Origin Source # stimes :: Integral b => b -> Q0Origin -> Q0Origin Source #
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 Source # sconcat :: NonEmpty Q1Origin -> Q1Origin Source # stimes :: Integral b => b -> Q1Origin -> Q1Origin Source #
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 Source # sconcat :: NonEmpty QωOrigin -> QωOrigin Source # stimes :: Integral b => b -> QωOrigin -> QωOrigin Source #
Semigroup MutualChecks Source # |
Instance details Defined in Agda.Syntax.Concrete.Definitions.Types Methods (<>) :: MutualChecks -> MutualChecks -> MutualChecks Source # sconcat :: NonEmpty MutualChecks -> MutualChecks Source # stimes :: Integral b => b -> MutualChecks -> MutualChecks Source #
Semigroup PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (<>) :: PatInfo -> PatInfo -> PatInfo Source # sconcat :: NonEmpty PatInfo -> PatInfo Source # stimes :: Integral b => b -> PatInfo -> PatInfo Source #
Semigroup Blocker Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (<>) :: Blocker -> Blocker -> Blocker Source # sconcat :: NonEmpty Blocker -> Blocker Source # stimes :: Integral b => b -> Blocker -> Blocker Source #
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 Source # sconcat :: NonEmpty NameMapEntry -> NameMapEntry Source # stimes :: Integral b => b -> NameMapEntry -> NameMapEntry Source #
Semigroup CallPath Source # |
Instance details Defined in Agda.Termination.Monad Methods (<>) :: CallPath -> CallPath -> CallPath Source # sconcat :: NonEmpty CallPath -> CallPath Source # stimes :: Integral b => b -> CallPath -> CallPath Source #
Semigroup VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods (<>) :: VarCounts -> VarCounts -> VarCounts Source # sconcat :: NonEmpty VarCounts -> VarCounts Source # stimes :: Integral b => b -> VarCounts -> VarCounts Source #
Semigroup FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: FlexRigMap -> FlexRigMap -> FlexRigMap Source # sconcat :: NonEmpty FlexRigMap -> FlexRigMap Source # stimes :: Integral b => b -> FlexRigMap -> FlexRigMap Source #
Semigroup MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: MetaSet -> MetaSet -> MetaSet Source # sconcat :: NonEmpty MetaSet -> MetaSet Source # stimes :: Integral b => b -> MetaSet -> MetaSet Source #
Semigroup ReduceDefs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: ReduceDefs -> ReduceDefs -> ReduceDefs Source # sconcat :: NonEmpty ReduceDefs -> ReduceDefs Source # stimes :: Integral b => b -> ReduceDefs -> ReduceDefs Source #
Semigroup Simplification Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (<>) :: Simplification -> Simplification -> Simplification Source # sconcat :: NonEmpty Simplification -> Simplification Source # stimes :: Integral b => b -> Simplification -> Simplification Source #
Semigroup OccurrencesBuilder Source # | The semigroup laws only hold up to flattening of `Concat`.
Instance details Defined in Agda.TypeChecking.Positivity Methods (<>) :: OccurrencesBuilder -> OccurrencesBuilder -> OccurrencesBuilder Source # sconcat :: NonEmpty OccurrencesBuilder -> OccurrencesBuilder Source # stimes :: Integral b => b -> OccurrencesBuilder -> OccurrencesBuilder Source #
Semigroup ClausesPostChecks Source # |
Instance details Defined in Agda.TypeChecking.Rules.Def Methods (<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks Source # sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks Source # stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks Source #
Semigroup FlexChoice Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: FlexChoice -> FlexChoice -> FlexChoice Source # sconcat :: NonEmpty FlexChoice -> FlexChoice Source # stimes :: Integral b => b -> FlexChoice -> FlexChoice Source #
Semigroup LeftoverPatterns Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns Source # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns Source # stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns Source #
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 Source # sconcat :: NonEmpty AbsolutePath -> AbsolutePath Source # stimes :: Integral b => b -> AbsolutePath -> AbsolutePath Source #
Semigroup IntSet Source # |
Instance details Defined in Agda.Utils.IntSet.Infinite Methods (<>) :: IntSet -> IntSet -> IntSet Source # sconcat :: NonEmpty IntSet -> IntSet Source # stimes :: Integral b => b -> IntSet -> IntSet Source #
Semigroup MaxNat Source # |
Instance details Defined in Agda.Utils.Monoid Methods (<>) :: MaxNat -> MaxNat -> MaxNat Source # sconcat :: NonEmpty MaxNat -> MaxNat Source # stimes :: Integral b => b -> MaxNat -> MaxNat Source #
Semigroup PartialOrdering Source # | Partial ordering forms a monoid under sequencing.
Instance details Defined in Agda.Utils.PartialOrd Methods (<>) :: PartialOrdering -> PartialOrdering -> PartialOrdering Source # sconcat :: NonEmpty PartialOrdering -> PartialOrdering Source # stimes :: Integral b => b -> PartialOrdering -> PartialOrdering Source #
Semigroup Series |
Instance details Defined in Data.Aeson.Encoding.Internal Methods (<>) :: Series -> Series -> Series Source # sconcat :: NonEmpty Series -> Series Source # stimes :: Integral b => b -> Series -> Series Source #
Semigroup Key |
Instance details Defined in Data.Aeson.Key Methods (<>) :: Key -> Key -> Key Source # sconcat :: NonEmpty Key -> Key Source # stimes :: Integral b => b -> Key -> Key Source #
Semigroup More |
Instance details Defined in Data.Attoparsec.Internal.Types Methods (<>) :: More -> More -> More Source # sconcat :: NonEmpty More -> More Source # stimes :: Integral b => b -> More -> More Source #
Semigroup All | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: All -> All -> All Source # sconcat :: NonEmpty All -> All Source # stimes :: Integral b => b -> All -> All Source #
Semigroup Any | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Any -> Any -> Any Source # sconcat :: NonEmpty Any -> Any Source # stimes :: Integral b => b -> Any -> Any Source #
Semigroup Void | Since: base-4.9.0.0
Instance details Defined in Data.Void Methods (<>) :: Void -> Void -> Void Source # sconcat :: NonEmpty Void -> Void Source # stimes :: Integral b => b -> Void -> Void Source #
Semigroup Attribute |
Instance details Defined in Text.Blaze.Internal Methods (<>) :: Attribute -> Attribute -> Attribute Source # sconcat :: NonEmpty Attribute -> Attribute Source # stimes :: Integral b => b -> Attribute -> Attribute Source #
Semigroup AttributeValue |
Instance details Defined in Text.Blaze.Internal Methods (<>) :: AttributeValue -> AttributeValue -> AttributeValue Source # sconcat :: NonEmpty AttributeValue -> AttributeValue Source # stimes :: Integral b => b -> AttributeValue -> AttributeValue Source #
Semigroup ChoiceString |
Instance details Defined in Text.Blaze.Internal Methods (<>) :: ChoiceString -> ChoiceString -> ChoiceString Source # sconcat :: NonEmpty ChoiceString -> ChoiceString Source # stimes :: Integral b => b -> ChoiceString -> ChoiceString Source #
Semigroup Builder |
Instance details Defined in Data.ByteString.Builder.Internal Methods (<>) :: Builder -> Builder -> Builder Source # sconcat :: NonEmpty Builder -> Builder Source # stimes :: Integral b => b -> Builder -> Builder Source #
Semigroup ByteString |
Instance details Defined in Data.ByteString.Internal Methods (<>) :: ByteString -> ByteString -> ByteString Source # sconcat :: NonEmpty ByteString -> ByteString Source # stimes :: Integral b => b -> ByteString -> ByteString Source #
Semigroup ByteString |
Instance details Defined in Data.ByteString.Lazy.Internal Methods (<>) :: ByteString -> ByteString -> ByteString Source # sconcat :: NonEmpty ByteString -> ByteString Source # stimes :: Integral b => b -> ByteString -> ByteString Source #
Semigroup ShortByteString |
Instance details Defined in Data.ByteString.Short.Internal Methods (<>) :: ShortByteString -> ShortByteString -> ShortByteString Source # sconcat :: NonEmpty ShortByteString -> ShortByteString Source # stimes :: Integral b => b -> ShortByteString -> ShortByteString Source #
Semigroup IntSet | Since: containers-0.5.7
Instance details Defined in Data.IntSet.Internal Methods (<>) :: IntSet -> IntSet -> IntSet Source # sconcat :: NonEmpty IntSet -> IntSet Source # stimes :: Integral b => b -> IntSet -> IntSet Source #
Semigroup Ordering | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: Ordering -> Ordering -> Ordering Source # sconcat :: NonEmpty Ordering -> Ordering Source # stimes :: Integral b => b -> Ordering -> Ordering Source #
Semigroup Slot |
Instance details Defined in Data.HashTable.ST.Basic Methods (<>) :: Slot -> Slot -> Slot Source # sconcat :: NonEmpty Slot -> Slot Source # stimes :: Integral b => b -> Slot -> Slot Source #
Semigroup Doc |
Instance details Defined in Text.PrettyPrint.HughesPJ Methods (<>) :: Doc -> Doc -> Doc Source # sconcat :: NonEmpty Doc -> Doc Source # stimes :: Integral b => b -> Doc -> Doc Source #
Semigroup ByteArray |
Instance details Defined in Data.Primitive.ByteArray Methods (<>) :: ByteArray -> ByteArray -> ByteArray Source # sconcat :: NonEmpty ByteArray -> ByteArray Source # stimes :: Integral b => b -> ByteArray -> ByteArray Source #
Semigroup ShortText |
Instance details Defined in Data.Text.Short.Internal Methods (<>) :: ShortText -> ShortText -> ShortText Source # sconcat :: NonEmpty ShortText -> ShortText Source # stimes :: Integral b => b -> ShortText -> ShortText Source #
Semigroup CalendarDiffDays | Additive
Instance details Defined in Data.Time.Calendar.CalendarDiffDays Methods (<>) :: CalendarDiffDays -> CalendarDiffDays -> CalendarDiffDays Source # sconcat :: NonEmpty CalendarDiffDays -> CalendarDiffDays Source # stimes :: Integral b => b -> CalendarDiffDays -> CalendarDiffDays Source #
Semigroup CalendarDiffTime | Additive
Instance details Defined in Data.Time.LocalTime.Internal.CalendarDiffTime Methods (<>) :: CalendarDiffTime -> CalendarDiffTime -> CalendarDiffTime Source # sconcat :: NonEmpty CalendarDiffTime -> CalendarDiffTime Source # stimes :: Integral b => b -> CalendarDiffTime -> CalendarDiffTime Source #
Semigroup () | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: () -> () -> () Source # sconcat :: NonEmpty () -> () Source # stimes :: Integral b => b -> () -> () Source #
Semigroup (DelayedMerge hl) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl Source # sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl Source # stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl Source #
Semigroup (UnderAddition Cohesion) Source # | `Cohesion` forms a semigroup under addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Cohesion -> UnderAddition Cohesion -> UnderAddition Cohesion Source # sconcat :: NonEmpty (UnderAddition Cohesion) -> UnderAddition Cohesion Source # stimes :: Integral b => b -> UnderAddition Cohesion -> UnderAddition Cohesion Source #
Semigroup (UnderAddition Modality) Source # | Pointwise addition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Modality -> UnderAddition Modality -> UnderAddition Modality Source # sconcat :: NonEmpty (UnderAddition Modality) -> UnderAddition Modality Source # stimes :: Integral b => b -> UnderAddition Modality -> UnderAddition Modality Source #
Semigroup (UnderAddition Quantity) Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Quantity -> UnderAddition Quantity -> UnderAddition Quantity Source # sconcat :: NonEmpty (UnderAddition Quantity) -> UnderAddition Quantity Source # stimes :: Integral b => b -> UnderAddition Quantity -> UnderAddition Quantity Source #
Semigroup (UnderAddition Relevance) Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderAddition Relevance -> UnderAddition Relevance -> UnderAddition Relevance Source # sconcat :: NonEmpty (UnderAddition Relevance) -> UnderAddition Relevance Source # stimes :: Integral b => b -> UnderAddition Relevance -> UnderAddition Relevance Source #
Semigroup (UnderComposition Cohesion) Source # | `Cohesion` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Cohesion -> UnderComposition Cohesion -> UnderComposition Cohesion Source # sconcat :: NonEmpty (UnderComposition Cohesion) -> UnderComposition Cohesion Source # stimes :: Integral b => b -> UnderComposition Cohesion -> UnderComposition Cohesion Source #
Semigroup (UnderComposition Erased) Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Erased -> UnderComposition Erased -> UnderComposition Erased Source # sconcat :: NonEmpty (UnderComposition Erased) -> UnderComposition Erased Source # stimes :: Integral b => b -> UnderComposition Erased -> UnderComposition Erased Source #
Semigroup (UnderComposition Modality) Source # | Pointwise composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Modality -> UnderComposition Modality -> UnderComposition Modality Source # sconcat :: NonEmpty (UnderComposition Modality) -> UnderComposition Modality Source # stimes :: Integral b => b -> UnderComposition Modality -> UnderComposition Modality Source #
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 Source # sconcat :: NonEmpty (UnderComposition Quantity) -> UnderComposition Quantity Source # stimes :: Integral b => b -> UnderComposition Quantity -> UnderComposition Quantity Source #
Semigroup (UnderComposition Relevance) Source # | `Relevance` forms a semigroup under composition.
Instance details Defined in Agda.Syntax.Common Methods (<>) :: UnderComposition Relevance -> UnderComposition Relevance -> UnderComposition Relevance Source # sconcat :: NonEmpty (UnderComposition Relevance) -> UnderComposition Relevance Source # stimes :: Integral b => b -> UnderComposition Relevance -> UnderComposition Relevance Source #
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 Source # sconcat :: NonEmpty (NotBlocked' t) -> NotBlocked' t Source # stimes :: Integral b => b -> NotBlocked' t -> NotBlocked' t Source #
Semigroup a => Semigroup (Range' a) Source # |
Instance details Defined in Agda.Syntax.Position Methods (<>) :: Range' a -> Range' a -> Range' a Source # sconcat :: NonEmpty (Range' a) -> Range' a Source # stimes :: Integral b => b -> Range' a -> Range' a Source #
Semigroup (CallGraph cinfo) Source # | `CallGraph` is a monoid under `union`.
Instance details Defined in Agda.Termination.CallGraph Methods (<>) :: CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo Source # sconcat :: NonEmpty (CallGraph cinfo) -> CallGraph cinfo Source # stimes :: Integral b => b -> CallGraph cinfo -> CallGraph cinfo Source #
Semigroup (CMSet cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods (<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo Source # sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo Source # stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo Source #
Semigroup m => Semigroup (TerM m) Source # |
Instance details Defined in Agda.Termination.Monad Methods (<>) :: TerM m -> TerM m -> TerM m Source # sconcat :: NonEmpty (TerM m) -> TerM m Source # stimes :: Integral b => b -> TerM m -> TerM m Source #
Semigroup m => Semigroup (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: Case m -> Case m -> Case m Source # sconcat :: NonEmpty (Case m) -> Case m Source # stimes :: Integral b => b -> Case m -> Case m Source #
Semigroup c => Semigroup (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: WithArity c -> WithArity c -> WithArity c Source # sconcat :: NonEmpty (WithArity c) -> WithArity c Source # stimes :: Integral b => b -> WithArity c -> WithArity c Source #
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 Source # sconcat :: NonEmpty (VarMap' a) -> VarMap' a Source # stimes :: Integral b => b -> VarMap' a -> VarMap' a Source #

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 Source # sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a Source # stimes :: Integral b => b -> VarOcc' a -> VarOcc' a Source #
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 Source # sconcat :: NonEmpty (TCM Doc) -> TCM Doc Source # stimes :: Integral b => b -> TCM Doc -> TCM Doc Source #
Semigroup (Match a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods (<>) :: Match a -> Match a -> Match a Source # sconcat :: NonEmpty (Match a) -> Match a Source # stimes :: Integral b => b -> Match a -> Match a Source #
Ord a => Semigroup (Bag a) Source # |
Instance details Defined in Agda.Utils.Bag Methods (<>) :: Bag a -> Bag a -> Bag a Source # sconcat :: NonEmpty (Bag a) -> Bag a Source # stimes :: Integral b => b -> Bag a -> Bag a Source #
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 Source # sconcat :: NonEmpty (Favorites a) -> Favorites a Source # stimes :: Integral b => b -> Favorites a -> Favorites a Source #
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 Source # sconcat :: NonEmpty (RangeMap a) -> RangeMap a Source # stimes :: Integral b => b -> RangeMap a -> RangeMap a Source #
Semigroup (KeyMap v) |
Instance details Defined in Data.Aeson.KeyMap Methods (<>) :: KeyMap v -> KeyMap v -> KeyMap v Source # sconcat :: NonEmpty (KeyMap v) -> KeyMap v Source # stimes :: Integral b => b -> KeyMap v -> KeyMap v Source #
Semigroup (IResult a) |
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: IResult a -> IResult a -> IResult a Source # sconcat :: NonEmpty (IResult a) -> IResult a Source # stimes :: Integral b => b -> IResult a -> IResult a Source #
Semigroup (Parser a) |
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Parser a -> Parser a -> Parser a Source # sconcat :: NonEmpty (Parser a) -> Parser a Source # stimes :: Integral b => b -> Parser a -> Parser a Source #
Semigroup (Result a) |
Instance details Defined in Data.Aeson.Types.Internal Methods (<>) :: Result a -> Result a -> Result a Source # sconcat :: NonEmpty (Result a) -> Result a Source # stimes :: Integral b => b -> Result a -> Result a Source #
Semigroup a => Semigroup (Concurrently a) | Only defined by `async` for `base >= 4.9` Since: async-2.1.0
Instance details Defined in Control.Concurrent.Async Methods (<>) :: Concurrently a -> Concurrently a -> Concurrently a Source # sconcat :: NonEmpty (Concurrently a) -> Concurrently a Source # stimes :: Integral b => b -> Concurrently a -> Concurrently a Source #
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 Source # sconcat :: NonEmpty (Identity a) -> Identity a Source # stimes :: Integral b => b -> Identity a -> Identity a Source #
Semigroup (First a) | Since: base-4.9.0.0
Instance details Defined in Data.Monoid Methods (<>) :: First a -> First a -> First a Source # sconcat :: NonEmpty (First a) -> First a Source # stimes :: Integral b => b -> First a -> First a Source #
Semigroup (Last a) | Since: base-4.9.0.0
Instance details Defined in Data.Monoid Methods (<>) :: Last a -> Last a -> Last a Source # sconcat :: NonEmpty (Last a) -> Last a Source # stimes :: Integral b => b -> Last a -> Last a Source #
Semigroup a => Semigroup (Down a) | Since: base-4.11.0.0
Instance details Defined in Data.Ord Methods (<>) :: Down a -> Down a -> Down a Source # sconcat :: NonEmpty (Down a) -> Down a Source # stimes :: Integral b => b -> Down a -> Down a Source #
Semigroup (First a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: First a -> First a -> First a Source # sconcat :: NonEmpty (First a) -> First a Source # stimes :: Integral b => b -> First a -> First a Source #
Semigroup (Last a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Last a -> Last a -> Last a Source # sconcat :: NonEmpty (Last a) -> Last a Source # stimes :: Integral b => b -> Last a -> Last a Source #
Ord a => Semigroup (Max a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Max a -> Max a -> Max a Source # sconcat :: NonEmpty (Max a) -> Max a Source # stimes :: Integral b => b -> Max a -> Max a Source #
Ord a => Semigroup (Min a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Min a -> Min a -> Min a Source # sconcat :: NonEmpty (Min a) -> Min a Source # stimes :: Integral b => b -> Min a -> Min a Source #
Semigroup a => Semigroup (Option a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: Option a -> Option a -> Option a Source # sconcat :: NonEmpty (Option a) -> Option a Source # stimes :: Integral b => b -> Option a -> Option a Source #
Monoid m => Semigroup (WrappedMonoid m) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup Methods (<>) :: WrappedMonoid m -> WrappedMonoid m -> WrappedMonoid m Source # sconcat :: NonEmpty (WrappedMonoid m) -> WrappedMonoid m Source # stimes :: Integral b => b -> WrappedMonoid m -> WrappedMonoid m Source #
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 Source # sconcat :: NonEmpty (Dual a) -> Dual a Source # stimes :: Integral b => b -> Dual a -> Dual a Source #
Semigroup (Endo a) | Since: base-4.9.0.0
Instance details Defined in Data.Semigroup.Internal Methods (<>) :: Endo a -> Endo a -> Endo a Source # sconcat :: NonEmpty (Endo a) -> Endo a Source # stimes :: Integral b => b -> Endo a -> Endo a Source #
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 Source # sconcat :: NonEmpty (Product a) -> Product a Source # stimes :: Integral b => b -> Product a -> Product a Source #
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 Source # sconcat :: NonEmpty (Sum a) -> Sum a Source # stimes :: Integral b => b -> Sum a -> Sum a Source #
Semigroup (NonEmpty a) | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: NonEmpty a -> NonEmpty a -> NonEmpty a Source # sconcat :: NonEmpty (NonEmpty a) -> NonEmpty a Source # stimes :: Integral b => b -> NonEmpty a -> NonEmpty a Source #
Semigroup p => Semigroup (Par1 p) | Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: Par1 p -> Par1 p -> Par1 p Source # sconcat :: NonEmpty (Par1 p) -> Par1 p Source # stimes :: Integral b => b -> Par1 p -> Par1 p Source #
Semigroup (PutM ()) |
Instance details Defined in Data.Binary.Put Methods (<>) :: PutM () -> PutM () -> PutM () Source # sconcat :: NonEmpty (PutM ()) -> PutM () Source # stimes :: Integral b => b -> PutM () -> PutM () Source #
Monoid a => Semigroup (MarkupM a) |
Instance details Defined in Text.Blaze.Internal Methods (<>) :: MarkupM a -> MarkupM a -> MarkupM a Source # sconcat :: NonEmpty (MarkupM a) -> MarkupM a Source # stimes :: Integral b => b -> MarkupM a -> MarkupM a Source #
Semigroup s => Semigroup (CI s) |
Instance details Defined in Data.CaseInsensitive.Internal Methods (<>) :: CI s -> CI s -> CI s Source # sconcat :: NonEmpty (CI s) -> CI s Source # stimes :: Integral b => b -> CI s -> CI s Source #
Semigroup (IntMap a) | Since: containers-0.5.7
Instance details Defined in Data.IntMap.Internal Methods (<>) :: IntMap a -> IntMap a -> IntMap a Source # sconcat :: NonEmpty (IntMap a) -> IntMap a Source # stimes :: Integral b => b -> IntMap a -> IntMap a Source #
Semigroup (Seq a) | Since: containers-0.5.7
Instance details Defined in Data.Sequence.Internal Methods (<>) :: Seq a -> Seq a -> Seq a Source # sconcat :: NonEmpty (Seq a) -> Seq a Source # stimes :: Integral b => b -> Seq a -> Seq a Source #
Semigroup (MergeSet a) |
Instance details Defined in Data.Set.Internal Methods (<>) :: MergeSet a -> MergeSet a -> MergeSet a Source # sconcat :: NonEmpty (MergeSet a) -> MergeSet a Source # stimes :: Integral b => b -> MergeSet a -> MergeSet a Source #
Ord a => Semigroup (Set a) | Since: containers-0.5.7
Instance details Defined in Data.Set.Internal Methods (<>) :: Set a -> Set a -> Set a Source # sconcat :: NonEmpty (Set a) -> Set a Source # stimes :: Integral b => b -> Set a -> Set a Source #
Semigroup (DNonEmpty a) |
Instance details Defined in Data.DList.DNonEmpty.Internal Methods (<>) :: DNonEmpty a -> DNonEmpty a -> DNonEmpty a Source # sconcat :: NonEmpty (DNonEmpty a) -> DNonEmpty a Source # stimes :: Integral b => b -> DNonEmpty a -> DNonEmpty a Source #
Semigroup (DList a) |
Instance details Defined in Data.DList.Internal Methods (<>) :: DList a -> DList a -> DList a Source # sconcat :: NonEmpty (DList a) -> DList a Source # stimes :: Integral b => b -> DList a -> DList a Source #
Semigroup a => Semigroup (IO a) | Since: base-4.10.0.0
Instance details Defined in GHC.Base Methods (<>) :: IO a -> IO a -> IO a Source # sconcat :: NonEmpty (IO a) -> IO a Source # stimes :: Integral b => b -> IO a -> IO a Source #
Semigroup (Doc a) |
Instance details Defined in Text.PrettyPrint.Annotated.HughesPJ Methods (<>) :: Doc a -> Doc a -> Doc a Source # sconcat :: NonEmpty (Doc a) -> Doc a Source # stimes :: Integral b => b -> Doc a -> Doc a Source #
Semigroup (Array a) |
Instance details Defined in Data.Primitive.Array Methods (<>) :: Array a -> Array a -> Array a Source # sconcat :: NonEmpty (Array a) -> Array a Source # stimes :: Integral b => b -> Array a -> Array a Source #
Semigroup (PrimArray a) |
Instance details Defined in Data.Primitive.PrimArray Methods (<>) :: PrimArray a -> PrimArray a -> PrimArray a Source # sconcat :: NonEmpty (PrimArray a) -> PrimArray a Source # stimes :: Integral b => b -> PrimArray a -> PrimArray a Source #
Semigroup (SmallArray a) |
Instance details Defined in Data.Primitive.SmallArray Methods (<>) :: SmallArray a -> SmallArray a -> SmallArray a Source # sconcat :: NonEmpty (SmallArray a) -> SmallArray a Source # stimes :: Integral b => b -> SmallArray a -> SmallArray a Source #
Semigroup a => Semigroup (Maybe a) |
Instance details Defined in Data.Strict.Maybe Methods (<>) :: Maybe a -> Maybe a -> Maybe a Source # sconcat :: NonEmpty (Maybe a) -> Maybe a Source # stimes :: Integral b => b -> Maybe a -> Maybe a Source #
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 Source # sconcat :: NonEmpty (Q a) -> Q a Source # stimes :: Integral b => b -> Q a -> Q a Source #

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

`<>` = `union`

O(n+m)

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

#### Examples

Expand

    >>> fromList [1,2] <> fromList [2,3]
    fromList [1,2,3]

Instance details Defined in Data.HashSet.Internal Methods (<>) :: HashSet a -> HashSet a -> HashSet a Source # sconcat :: NonEmpty (HashSet a) -> HashSet a Source # stimes :: Integral b => b -> HashSet a -> HashSet a Source #
Semigroup (Vector a) |
Instance details Defined in Data.Vector Methods (<>) :: Vector a -> Vector a -> Vector a Source # sconcat :: NonEmpty (Vector a) -> Vector a Source # stimes :: Integral b => b -> Vector a -> Vector a Source #
Prim a => Semigroup (Vector a) |
Instance details Defined in Data.Vector.Primitive Methods (<>) :: Vector a -> Vector a -> Vector a Source # sconcat :: NonEmpty (Vector a) -> Vector a Source # stimes :: Integral b => b -> Vector a -> Vector a Source #
Storable a => Semigroup (Vector a) |
Instance details Defined in Data.Vector.Storable Methods (<>) :: Vector a -> Vector a -> Vector a Source # sconcat :: NonEmpty (Vector a) -> Vector a Source # stimes :: Integral b => b -> Vector a -> Vector a Source #
Semigroup a => Semigroup (Maybe a) | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: Maybe a -> Maybe a -> Maybe a Source # sconcat :: NonEmpty (Maybe a) -> Maybe a Source # stimes :: Integral b => b -> Maybe a -> Maybe a Source #
Semigroup a => Semigroup (a) | Since: base-4.15
Instance details Defined in GHC.Base Methods (<>) :: (a) -> (a) -> (a) Source # sconcat :: NonEmpty (a) -> (a) Source # stimes :: Integral b => b -> (a) -> (a) Source #
Semigroup [a] | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: [a] -> [a] -> [a] Source # sconcat :: NonEmpty [a] -> [a] Source # stimes :: Integral b => b -> [a] -> [a] Source #
(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 Source # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m Source # stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m Source #
Semigroup (Using' n m) Source # |
Instance details Defined in Agda.Syntax.Common Methods (<>) :: Using' n m -> Using' n m -> Using' n m Source # sconcat :: NonEmpty (Using' n m) -> Using' n m Source # stimes :: Integral b => b -> Using' n m -> Using' n m Source #
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 Source # sconcat :: NonEmpty (Blocked' t a) -> Blocked' t a Source # stimes :: Integral b => b -> Blocked' t a -> Blocked' t a Source #
(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 Source # sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a Source # stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a Source #
(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 Source # sconcat :: NonEmpty (TCMT m a) -> TCMT m a Source # stimes :: Integral b => b -> TCMT m a -> TCMT m a Source #
Monad m => Semigroup (ListT m a) Source # |
Instance details Defined in Agda.Utils.ListT Methods (<>) :: ListT m a -> ListT m a -> ListT m a Source # sconcat :: NonEmpty (ListT m a) -> ListT m a Source # stimes :: Integral b => b -> ListT m a -> ListT m a Source #
Semigroup (Parser i a) |
Instance details Defined in Data.Attoparsec.Internal.Types Methods (<>) :: Parser i a -> Parser i a -> Parser i a Source # sconcat :: NonEmpty (Parser i a) -> Parser i a Source # stimes :: Integral b => b -> Parser i a -> Parser i a Source #
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 Source # sconcat :: NonEmpty (Either a b) -> Either a b Source # stimes :: Integral b0 => b0 -> Either a b -> Either a b Source #
Semigroup (Proxy s) | Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s Source # sconcat :: NonEmpty (Proxy s) -> Proxy s Source # stimes :: Integral b => b -> Proxy s -> Proxy s Source #
Semigroup (U1 p) | Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: U1 p -> U1 p -> U1 p Source # sconcat :: NonEmpty (U1 p) -> U1 p Source # stimes :: Integral b => b -> U1 p -> U1 p Source #
Semigroup (V1 p) | Since: base-4.12.0.0
Instance details Defined in GHC.Generics Methods (<>) :: V1 p -> V1 p -> V1 p Source # sconcat :: NonEmpty (V1 p) -> V1 p Source # stimes :: Integral b => b -> V1 p -> V1 p Source #
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 Source # sconcat :: NonEmpty (ST s a) -> ST s a Source # stimes :: Integral b => b -> ST s a -> ST s a Source #
Ord k => Semigroup (Map k v) |
Instance details Defined in Data.Map.Internal Methods (<>) :: Map k v -> Map k v -> Map k v Source # sconcat :: NonEmpty (Map k v) -> Map k v Source # stimes :: Integral b => b -> Map k v -> Map k v Source #
Semigroup (Either a b) |
Instance details Defined in Data.Strict.Either Methods (<>) :: Either a b -> Either a b -> Either a b Source # sconcat :: NonEmpty (Either a b) -> Either a b Source # stimes :: Integral b0 => b0 -> Either a b -> Either a b Source #
(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 Source # sconcat :: NonEmpty (These a b) -> These a b Source # stimes :: Integral b0 => b0 -> These a b -> These a b Source #
(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 Source # sconcat :: NonEmpty (Pair a b) -> Pair a b Source # stimes :: Integral b0 => b0 -> Pair a b -> Pair a b Source #
(Semigroup a, Semigroup b) => Semigroup (These a b) |
Instance details Defined in Data.These Methods (<>) :: These a b -> These a b -> These a b Source # sconcat :: NonEmpty (These a b) -> These a b Source # stimes :: Integral b0 => b0 -> These a b -> These a b Source #

(Eq k, Hashable k) => Semigroup (HashMap k v)

`<>` = `union`

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

#### Examples

Expand

    >>> fromList [(1,'a'),(2,'b')] <> fromList [(2,'c'),(3,'d')]
    fromList [(1,'a'),(2,'b'),(3,'d')]

Instance details Defined in Data.HashMap.Internal Methods (<>) :: HashMap k v -> HashMap k v -> HashMap k v Source # sconcat :: NonEmpty (HashMap k v) -> HashMap k v Source # stimes :: Integral b => b -> HashMap k v -> HashMap k v Source #
Semigroup b => Semigroup (a -> b) | Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: (a -> b) -> (a -> b) -> a -> b Source # sconcat :: NonEmpty (a -> b) -> a -> b Source # stimes :: Integral b0 => b0 -> (a -> b) -> a -> b Source #
(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) Source # sconcat :: NonEmpty (a, b) -> (a, b) Source # stimes :: Integral b0 => b0 -> (a, b) -> (a, b) Source #
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 Source # sconcat :: NonEmpty (Const a b) -> Const a b Source # stimes :: Integral b0 => b0 -> Const a b -> Const a b Source #
(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 Source # sconcat :: NonEmpty (Ap f a) -> Ap f a Source # stimes :: Integral b => b -> Ap f a -> Ap f a Source #
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 Source # sconcat :: NonEmpty (Alt f a) -> Alt f a Source # stimes :: Integral b => b -> Alt f a -> Alt f a Source #
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 Source # sconcat :: NonEmpty (Rec1 f p) -> Rec1 f p Source # stimes :: Integral b => b -> Rec1 f p -> Rec1 f p Source #
Semigroup a => Semigroup (Tagged s a) |
Instance details Defined in Data.Tagged Methods (<>) :: Tagged s a -> Tagged s a -> Tagged s a Source # sconcat :: NonEmpty (Tagged s a) -> Tagged s a Source # stimes :: Integral b => b -> Tagged s a -> Tagged s a Source #
(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 Source # sconcat :: NonEmpty (ReaderT s m doc) -> ReaderT s m doc Source # stimes :: Integral b => b -> ReaderT s m doc -> ReaderT s m doc Source #
(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 Source # sconcat :: NonEmpty (StateT s m doc) -> StateT s m doc Source # stimes :: Integral b => b -> StateT s m doc -> StateT s m doc Source #
(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) Source # sconcat :: NonEmpty (a, b, c) -> (a, b, c) Source # stimes :: Integral b0 => b0 -> (a, b, c) -> (a, b, c) Source #
(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 Source # sconcat :: NonEmpty ((f :*: g) p) -> (f :*: g) p Source # stimes :: Integral b => b -> (f :*: g) p -> (f :*: g) p Source #
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 Source # sconcat :: NonEmpty (K1 i c p) -> K1 i c p Source # stimes :: Integral b => b -> K1 i c p -> K1 i c p Source #
(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) Source # sconcat :: NonEmpty (a, b, c, d) -> (a, b, c, d) Source # stimes :: Integral b0 => b0 -> (a, b, c, d) -> (a, b, c, d) Source #
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 Source # sconcat :: NonEmpty ((f :.: g) p) -> (f :.: g) p Source # stimes :: Integral b => b -> (f :.: g) p -> (f :.: g) p Source #
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 Source # sconcat :: NonEmpty (M1 i c f p) -> M1 i c f p Source # stimes :: Integral b => b -> M1 i c f p -> M1 i c f p Source #
(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) Source # sconcat :: NonEmpty (a, b, c, d, e) -> (a, b, c, d, e) Source # stimes :: Integral b0 => b0 -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

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 Source # sconcat :: NonEmpty (TCM Doc) -> TCM Doc Source # stimes :: Integral b => b -> TCM Doc -> TCM Doc Source #