Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Pretty

Synopsis

Documentation

($$) :: Applicative m => m Doc -> m Doc -> m Doc infixl 5 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 #

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

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

colon :: Applicative m => m Doc Source #

comma :: Applicative m => m Doc Source #

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

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

equals :: Applicative m => m Doc Source #

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

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

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

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

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

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

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

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

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

pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc Source #

pretty :: (Applicative m, Pretty a) => a -> 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 #

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

Comma-separated list in brackets.

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

prettyList without the brackets.

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

For unquote.

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

Pretty print with a given context precedence

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

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

Proper pretty printing of patterns:

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

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

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

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

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

sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a] Source #

sequenceAFoldable == sequenceA . Fold.toList

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

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

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

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

type Doc = Doc Source #

type MonadPretty (m :: Type -> Type) = 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 #

class PrettyTCM a where Source #

Methods

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

Instances

Instances details
PrettyTCM MimerResult Source # 
Instance details

Defined in Agda.Mimer.Mimer

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ModalPolarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM LHS Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

Defined in Agda.TypeChecking.Pretty

Methods

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

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM GHCBackendError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM InteractionError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM JSBackendError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM MissingTypeSignatureInfo Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

Defined in Agda.TypeChecking.Errors

Methods

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

PrettyTCM Warning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Polarity -> 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.Pretty

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

Methods

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

PrettyTCM SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Pretty

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

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Text -> 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 String) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Arg String -> 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, Subst a) => PrettyTCM (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Abs 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 (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => DiscrimTree 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 a => PrettyTCM (List1 a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => List1 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 (Set a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

PrettyTCM 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 x, PrettyTCM a) => PrettyTCM (Boundary' x a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Boundary' x 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 #

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

Preconditions to run the AbstractToConcrete translation.

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 #