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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Pretty

Contents

- Orphan instances

Synopsis

- pretty :: (Applicative m, Pretty a) => a -> m Doc
- text :: Applicative m => String -> m Doc
- (<?>) :: Applicative m => m Doc -> m Doc -> m Doc
- comma :: Applicative m => m Doc
- colon :: Applicative m => m Doc
- parens :: Functor m => m Doc -> m Doc
- (<+>) :: Applicative m => m Doc -> m Doc -> m Doc
- hcat :: (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
- vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- brackets :: Functor m => m Doc -> m Doc
- braces :: Functor m => m Doc -> m Doc
- type Doc = Doc
- equals :: Applicative m => m Doc
- quotes :: Functor m => m Doc -> m Doc
- doubleQuotes :: Functor m => m Doc -> m Doc
- nest :: Functor m => Int -> m Doc -> m Doc
- hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
- punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
- ($$) :: Applicative m => m Doc -> m Doc -> m Doc
- ($+$) :: Applicative m => m Doc -> m Doc -> m Doc
- sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- class PrettyTCM a where
  - prettyTCM :: MonadPretty m => a -> m Doc
- dbraces :: Functor m => m Doc -> m Doc
- prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
- prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
- type MonadPretty (m :: Type -> Type) = MonadAbsToCon m
- pshow :: (Applicative m, Show a) => a -> m Doc
- pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
- prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
- pwords :: Applicative m => String -> [m Doc]
- fwords :: Applicative m => String -> m Doc
- parensNonEmpty :: Functor m => m Doc -> m Doc
- multiLineText :: Applicative m => String -> m Doc
- newtype PrettyContext = PrettyContext Context
- prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
- sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
- superscript :: Applicative m => Int -> m Doc
- prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
- prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
- prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
- prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
- data WithNode n a = WithNode n a
- class PrettyTCMWithNode a where
  - prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
- 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))

# Documentation

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

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

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

comma :: Applicative m => m Doc Source #

colon :: Applicative m => m Doc Source #

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

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

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

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

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

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

type Doc = Doc Source #

equals :: Applicative m => m Doc Source #

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

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

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

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

punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (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 5 Source #

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

fsep :: (Applicative m, Foldable t) => t (m Doc) -> 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 #

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

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

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

`prettyList` without the brackets.

type MonadPretty (m :: Type -> Type) = MonadAbsToCon m Source #

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

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

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

Comma-separated list in brackets.

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

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

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

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

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 #

prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> 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 #

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

Pretty print with a given context precedence

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

Proper pretty printing of patterns:

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

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

For unquote.

data WithNode n a Source #

Pairing something with a node (for printing only).

Constructors

WithNode n a |

class PrettyTCMWithNode a where Source #

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

Methods

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

#### Instances

Instances details

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

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