Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Pretty

Contents

Orphan instances

Synopsis

($$) :: Applicative m => m Doc -> 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
braces :: Functor m => m Doc -> m Doc
brackets :: Functor m => m Doc -> m Doc
colon :: Applicative m => m Doc
comma :: Applicative m => m Doc
dbraces :: Functor m => m Doc -> m Doc
defnToNameKind :: Defn -> NameKind
doubleQuotes :: Functor m => m Doc -> m Doc
equals :: Applicative m => m Doc
fsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
fwords :: Applicative m => String -> m Doc
githubIssue :: Applicative m => Int -> m Doc
hang :: Applicative m => m Doc -> Int -> m Doc -> m Doc
hcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
hlArgument :: Functor m => m Doc -> m Doc
hlBound :: Functor m => m Doc -> m Doc
hlConstructor :: Functor m => Induction -> m Doc -> m Doc
hlDatatype :: Functor m => m Doc -> m Doc
hlField :: Functor m => m Doc -> m Doc
hlFunction :: Functor m => m Doc -> m Doc
hlGeneralizable :: Functor m => m Doc -> m Doc
hlMacro :: Functor m => m Doc -> m Doc
hlModule :: Functor m => m Doc -> m Doc
hlPostulate :: Functor m => m Doc -> m Doc
hlPrimitive :: Functor m => m Doc -> m Doc
hlRecord :: Functor m => m Doc -> m Doc
hsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
multiLineText :: Applicative m => String -> m Doc
nest :: Functor m => Int -> m Doc -> m Doc
parens :: Functor m => m Doc -> m Doc
parensNonEmpty :: Functor m => m Doc -> m Doc
pluralS :: (Functor m, Sized a) => a -> m Doc -> m Doc
pretty :: (Applicative m, Pretty a) => a -> 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
prettyList :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
prettyList_ :: (Applicative m, Semigroup (m Doc), Foldable t) => t (m Doc) -> m Doc
prettyR :: (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m, MonadError TCErr m) => r -> m Doc
prettyTCMCtx :: (PrettyTCM a, MonadPretty m) => Precedence -> a -> m Doc
prettyTCMPatternList :: MonadPretty m => [NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatterns :: MonadPretty m => [NamedArg DeBruijnPattern] -> m [Doc]
pshow :: (Applicative m, Show a) => a -> m Doc
punctuate :: (Applicative m, Semigroup (m Doc), Foldable t) => m Doc -> t (m Doc) -> [m Doc]
pwords :: Applicative m => String -> [m Doc]
quotes :: Functor m => m Doc -> m Doc
sep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
sequenceAFoldable :: (Applicative m, Foldable t) => t (m a) -> m [a]
superscript :: Applicative m => Int -> m Doc
text :: Applicative m => String -> m Doc
url :: Applicative m => String -> m Doc
vcat :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
vsep :: (Applicative m, Foldable t) => t (m Doc) -> m Doc
type Doc = Doc
type MonadPretty (m :: Type -> Type) = MonadAbsToCon m
newtype PrettyContext = PrettyContext Context
class PrettyTCM a where
- prettyTCM :: MonadPretty m => a -> m Doc
class PrettyTCMWithNode a where
- prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n a -> m Doc
data WithNode n a = WithNode n a
type MonadAbsToCon (m :: Type -> Type) = (MonadFileId m, MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

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 #

defnToNameKind :: Defn -> NameKind 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 #

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

Link to an issue on the Agda bug tracker.

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

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

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

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

hlConstructor :: Functor m => Induction -> m Doc -> m Doc Source #

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

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

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

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

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

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

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

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

hlRecord :: Functor m => 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 #

url :: 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 BaseComponents Source #
Instance details Defined in Agda.Mimer.Types Methods prettyTCM :: MonadPretty m => BaseComponents -> m Doc Source #
PrettyTCM Component Source #
Instance details Defined in Agda.Mimer.Types Methods prettyTCM :: MonadPretty m => Component -> m Doc Source #
PrettyTCM MimerResult Source #
Instance details Defined in Agda.Mimer.Types Methods prettyTCM :: MonadPretty m => MimerResult -> m Doc Source #
PrettyTCM SearchOptions Source #
Instance details Defined in Agda.Mimer.Types Methods prettyTCM :: MonadPretty m => SearchOptions -> 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 #	Automatically highlights the resulting document with the correct name kind.
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 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.SplitPattern 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 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 TopLevelModuleNameWithSourceFile Source #
Instance details Defined in Agda.TypeChecking.Errors Methods prettyTCM :: MonadPretty m => TopLevelModuleNameWithSourceFile -> 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 DigestedUnifyStep Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => DigestedUnifyStep -> 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) = (MonadFileId m, 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 #