Agda-2.6.2.2.20221128: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.Pretty

Description

Pretty printing functions.

Synopsis

Documentation

class Pretty a where Source #

While Show is for rendering data in Haskell syntax, Pretty is for displaying data to the world, i.e., the user and the environment.

Atomic data has no inner document structure, so just implement pretty as pretty a = text $ ... a ....

Minimal complete definition

Nothing

Methods

pretty :: a -> Doc Source #

prettyPrec :: Int -> a -> Doc Source #

prettyList :: [a] -> Doc Source #

Instances

Instances details
Pretty Phase Source # 
Instance details

Defined in Agda.Benchmarking

Methods

pretty :: Phase -> Doc Source #

prettyPrec :: Int -> Phase -> Doc Source #

prettyList :: [Phase] -> Doc Source #

Pretty HaskellPragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

pretty :: HaskellPragma -> Doc Source #

prettyPrec :: Int -> HaskellPragma -> Doc Source #

prettyList :: [HaskellPragma] -> Doc Source #

Pretty CompilerBackend Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

pretty :: CompilerBackend -> Doc Source #

prettyPrec :: Int -> CompilerBackend -> Doc Source #

prettyList :: [CompilerBackend] -> Doc Source #

Pretty InterfaceFile Source # 
Instance details

Defined in Agda.Interaction.FindFile

Methods

pretty :: InterfaceFile -> Doc Source #

prettyPrec :: Int -> InterfaceFile -> Doc Source #

prettyList :: [InterfaceFile] -> Doc Source #

Pretty SourceFile Source # 
Instance details

Defined in Agda.Interaction.FindFile

Methods

pretty :: SourceFile -> Doc Source #

prettyPrec :: Int -> SourceFile -> Doc Source #

prettyList :: [SourceFile] -> Doc Source #

Pretty LibError' Source #

Pretty-print library management error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibError' -> Doc Source #

prettyPrec :: Int -> LibError' -> Doc Source #

prettyList :: [LibError'] -> Doc Source #

Pretty LibParseError Source #

Print library file parse error without position info.

Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibParseError -> Doc Source #

prettyPrec :: Int -> LibParseError -> Doc Source #

prettyList :: [LibParseError] -> Doc Source #

Pretty LibWarning Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning -> Doc Source #

prettyPrec :: Int -> LibWarning -> Doc Source #

prettyList :: [LibWarning] -> Doc Source #

Pretty LibWarning' Source # 
Instance details

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning' -> Doc Source #

prettyPrec :: Int -> LibWarning' -> Doc Source #

prettyList :: [LibWarning'] -> Doc Source #

Pretty OptionWarning Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Methods

pretty :: OptionWarning -> Doc Source #

prettyPrec :: Int -> OptionWarning -> Doc Source #

prettyList :: [OptionWarning] -> Doc Source #

Pretty ScopeCopyInfo Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

pretty :: ScopeCopyInfo -> Doc Source #

prettyPrec :: Int -> ScopeCopyInfo -> Doc Source #

prettyList :: [ScopeCopyInfo] -> Doc Source #

Pretty AmbiguousQName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AmbiguousQName -> Doc Source #

prettyPrec :: Int -> AmbiguousQName -> Doc Source #

prettyList :: [AmbiguousQName] -> Doc Source #

Pretty ModuleName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: ModuleName -> Doc Source #

prettyPrec :: Int -> ModuleName -> Doc Source #

prettyList :: [ModuleName] -> Doc Source #

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc Source #

prettyPrec :: Int -> Name -> Doc Source #

prettyList :: [Name] -> Doc Source #

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QName -> Doc Source #

prettyPrec :: Int -> QName -> Doc Source #

prettyList :: [QName] -> Doc Source #

Pretty Suffix Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Suffix -> Doc Source #

prettyPrec :: Int -> Suffix -> Doc Source #

prettyList :: [Suffix] -> Doc Source #

Pretty Access Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Access -> Doc Source #

prettyPrec :: Int -> Access -> Doc Source #

prettyList :: [Access] -> Doc Source #

Pretty Associativity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Associativity -> Doc Source #

prettyPrec :: Int -> Associativity -> Doc Source #

prettyList :: [Associativity] -> Doc Source #

Pretty Cohesion Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Cohesion -> Doc Source #

prettyPrec :: Int -> Cohesion -> Doc Source #

prettyList :: [Cohesion] -> Doc Source #

Pretty FileType Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: FileType -> Doc Source #

prettyPrec :: Int -> FileType -> Doc Source #

prettyList :: [FileType] -> Doc Source #

Pretty Fixity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity -> Doc Source #

prettyPrec :: Int -> Fixity -> Doc Source #

prettyList :: [Fixity] -> Doc Source #

Pretty Fixity' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity' -> Doc Source #

prettyPrec :: Int -> Fixity' -> Doc Source #

prettyList :: [Fixity'] -> Doc Source #

Pretty FixityLevel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: FixityLevel -> Doc Source #

prettyPrec :: Int -> FixityLevel -> Doc Source #

prettyList :: [FixityLevel] -> Doc Source #

Pretty Hiding Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Hiding -> Doc Source #

prettyPrec :: Int -> Hiding -> Doc Source #

prettyList :: [Hiding] -> Doc Source #

Pretty Induction Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Induction -> Doc Source #

prettyPrec :: Int -> Induction -> Doc Source #

prettyList :: [Induction] -> Doc Source #

Pretty InteractionId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: InteractionId -> Doc Source #

prettyPrec :: Int -> InteractionId -> Doc Source #

prettyList :: [InteractionId] -> Doc Source #

Pretty MetaId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc Source #

prettyPrec :: Int -> MetaId -> Doc Source #

prettyList :: [MetaId] -> Doc Source #

Pretty Modality Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Modality -> Doc Source #

prettyPrec :: Int -> Modality -> Doc Source #

prettyList :: [Modality] -> Doc Source #

Pretty NameId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: NameId -> Doc Source #

prettyPrec :: Int -> NameId -> Doc Source #

prettyList :: [NameId] -> Doc Source #

Pretty NotationPart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NotationPart -> Doc Source #

prettyPrec :: Int -> NotationPart -> Doc Source #

prettyList :: [NotationPart] -> Doc Source #

Pretty ProblemId Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: ProblemId -> Doc Source #

prettyPrec :: Int -> ProblemId -> Doc Source #

prettyList :: [ProblemId] -> Doc Source #

Pretty Q0Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q0Origin -> Doc Source #

prettyPrec :: Int -> Q0Origin -> Doc Source #

prettyList :: [Q0Origin] -> Doc Source #

Pretty Q1Origin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q1Origin -> Doc Source #

prettyPrec :: Int -> Q1Origin -> Doc Source #

prettyList :: [Q1Origin] -> Doc Source #

Pretty Quantity Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Quantity -> Doc Source #

prettyPrec :: Int -> Quantity -> Doc Source #

prettyList :: [Quantity] -> Doc Source #

Pretty QωOrigin Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: QωOrigin -> Doc Source #

prettyPrec :: Int -> QωOrigin -> Doc Source #

prettyList :: [QωOrigin] -> Doc Source #

Pretty Relevance Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Relevance -> Doc Source #

prettyPrec :: Int -> Relevance -> Doc Source #

prettyList :: [Relevance] -> Doc Source #

Pretty BoundName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: BoundName -> Doc Source #

prettyPrec :: Int -> BoundName -> Doc Source #

prettyList :: [BoundName] -> Doc Source #

Pretty Declaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Declaration -> Doc Source #

prettyPrec :: Int -> Declaration -> Doc Source #

prettyList :: [Declaration] -> Doc Source #

Pretty DoStmt Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: DoStmt -> Doc Source #

prettyPrec :: Int -> DoStmt -> Doc Source #

prettyList :: [DoStmt] -> Doc Source #

Pretty Expr Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc Source #

prettyPrec :: Int -> Expr -> Doc Source #

prettyList :: [Expr] -> Doc Source #

Pretty LHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc Source #

prettyPrec :: Int -> LHS -> Doc Source #

prettyList :: [LHS] -> Doc Source #

Pretty LHSCore Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHSCore -> Doc Source #

prettyPrec :: Int -> LHSCore -> Doc Source #

prettyList :: [LHSCore] -> Doc Source #

Pretty LamBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc Source #

prettyPrec :: Int -> LamBinding -> Doc Source #

prettyList :: [LamBinding] -> Doc Source #

Pretty LamClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamClause -> Doc Source #

prettyPrec :: Int -> LamClause -> Doc Source #

prettyList :: [LamClause] -> Doc Source #

Pretty ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleApplication -> Doc Source #

prettyPrec :: Int -> ModuleApplication -> Doc Source #

prettyList :: [ModuleApplication] -> Doc Source #

Pretty ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleAssignment -> Doc Source #

prettyPrec :: Int -> ModuleAssignment -> Doc Source #

prettyList :: [ModuleAssignment] -> Doc Source #

Pretty OpenShortHand Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpenShortHand -> Doc Source #

prettyPrec :: Int -> OpenShortHand -> Doc Source #

prettyList :: [OpenShortHand] -> Doc Source #

Pretty Pattern Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pattern -> Doc Source #

prettyPrec :: Int -> Pattern -> Doc Source #

prettyList :: [Pattern] -> Doc Source #

Pretty Pragma Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pragma -> Doc Source #

prettyPrec :: Int -> Pragma -> Doc Source #

prettyList :: [Pragma] -> Doc Source #

Pretty RHS Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc Source #

prettyPrec :: Int -> RHS -> Doc Source #

prettyList :: [RHS] -> Doc Source #

Pretty TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc Source #

prettyPrec :: Int -> TypedBinding -> Doc Source #

prettyList :: [TypedBinding] -> Doc Source #

Pretty WhereClause Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc Source #

prettyPrec :: Int -> WhereClause -> Doc Source #

prettyList :: [WhereClause] -> Doc Source #

Pretty DeclarationException' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationException' -> Doc Source #

prettyPrec :: Int -> DeclarationException' -> Doc Source #

prettyList :: [DeclarationException'] -> Doc Source #

Pretty DeclarationWarning Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning -> Doc Source #

prettyPrec :: Int -> DeclarationWarning -> Doc Source #

prettyList :: [DeclarationWarning] -> Doc Source #

Pretty DeclarationWarning' Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning' -> Doc Source #

prettyPrec :: Int -> DeclarationWarning' -> Doc Source #

prettyList :: [DeclarationWarning'] -> Doc Source #

Pretty DataRecOrFun Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

pretty :: DataRecOrFun -> Doc Source #

prettyPrec :: Int -> DataRecOrFun -> Doc Source #

prettyList :: [DataRecOrFun] -> Doc Source #

Pretty NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

pretty :: NiceDeclaration -> Doc Source #

prettyPrec :: Int -> NiceDeclaration -> Doc Source #

prettyList :: [NiceDeclaration] -> Doc Source #

Pretty Name Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc Source #

prettyPrec :: Int -> Name -> Doc Source #

prettyList :: [Name] -> Doc Source #

Pretty NamePart Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc Source #

prettyPrec :: Int -> NamePart -> Doc Source #

prettyList :: [NamePart] -> Doc Source #

Pretty QName Source # 
Instance details

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: QName -> Doc Source #

prettyPrec :: Int -> QName -> Doc Source #

prettyList :: [QName] -> Doc Source #

Pretty NamedBinding Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NamedBinding -> Doc Source #

prettyPrec :: Int -> NamedBinding -> Doc Source #

prettyList :: [NamedBinding] -> Doc Source #

Pretty Tel Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc Source #

prettyPrec :: Int -> Tel -> Doc Source #

prettyList :: [Tel] -> Doc Source #

Pretty Precedence Source # 
Instance details

Defined in Agda.Syntax.Fixity

Methods

pretty :: Precedence -> Doc Source #

prettyPrec :: Int -> Precedence -> Doc Source #

prettyList :: [Precedence] -> Doc Source #

Pretty Clause Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc Source #

prettyPrec :: Int -> Clause -> Doc Source #

prettyList :: [Clause] -> Doc Source #

Pretty ConHead Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc Source #

prettyPrec :: Int -> ConHead -> Doc Source #

prettyList :: [ConHead] -> Doc Source #

Pretty DBPatVar Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc Source #

prettyPrec :: Int -> DBPatVar -> Doc Source #

prettyList :: [DBPatVar] -> Doc Source #

Pretty Level Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc Source #

prettyPrec :: Int -> Level -> Doc Source #

prettyList :: [Level] -> Doc Source #

Pretty PlusLevel Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc Source #

prettyPrec :: Int -> PlusLevel -> Doc Source #

prettyList :: [PlusLevel] -> Doc Source #

Pretty Sort Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc Source #

prettyPrec :: Int -> Sort -> Doc Source #

prettyList :: [Sort] -> Doc Source #

Pretty Term Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc Source #

prettyPrec :: Int -> Term -> Doc Source #

prettyList :: [Term] -> Doc Source #

Pretty Type Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc Source #

prettyPrec :: Int -> Type -> Doc Source #

prettyList :: [Type] -> Doc Source #

Pretty Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

Methods

pretty :: Blocker -> Doc Source #

prettyPrec :: Int -> Blocker -> Doc Source #

prettyList :: [Blocker] -> Doc Source #

Pretty Literal Source # 
Instance details

Defined in Agda.Syntax.Literal

Methods

pretty :: Literal -> Doc Source #

prettyPrec :: Int -> Literal -> Doc Source #

prettyList :: [Literal] -> Doc Source #

Pretty NewNotation Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

pretty :: NewNotation -> Doc Source #

prettyPrec :: Int -> NewNotation -> Doc Source #

prettyList :: [NewNotation] -> Doc Source #

Pretty NotationKind Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationKind -> Doc Source #

prettyPrec :: Int -> NotationKind -> Doc Source #

prettyList :: [NotationKind] -> Doc Source #

Pretty NotationSection Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationSection -> Doc Source #

prettyPrec :: Int -> NotationSection -> Doc Source #

prettyList :: [NotationSection] -> Doc Source #

Pretty ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseError -> Doc Source #

prettyPrec :: Int -> ParseError -> Doc Source #

prettyList :: [ParseError] -> Doc Source #

Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseWarning -> Doc Source #

prettyPrec :: Int -> ParseWarning -> Doc Source #

prettyList :: [ParseWarning] -> Doc Source #

Pretty IntervalWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: IntervalWithoutFile -> Doc Source #

prettyPrec :: Int -> IntervalWithoutFile -> Doc Source #

prettyList :: [IntervalWithoutFile] -> Doc Source #

Pretty PositionWithoutFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: PositionWithoutFile -> Doc Source #

prettyPrec :: Int -> PositionWithoutFile -> Doc Source #

prettyList :: [PositionWithoutFile] -> Doc Source #

Pretty RangeFile Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: RangeFile -> Doc Source #

prettyPrec :: Int -> RangeFile -> Doc Source #

prettyList :: [RangeFile] -> Doc Source #

Pretty AbstractModule Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractModule -> Doc Source #

prettyPrec :: Int -> AbstractModule -> Doc Source #

prettyList :: [AbstractModule] -> Doc Source #

Pretty AbstractName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractName -> Doc Source #

prettyPrec :: Int -> AbstractName -> Doc Source #

prettyList :: [AbstractName] -> Doc Source #

Pretty BindingSource Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: BindingSource -> Doc Source #

prettyPrec :: Int -> BindingSource -> Doc Source #

prettyList :: [BindingSource] -> Doc Source #

Pretty LocalVar Source #

We show shadowed variables as prefixed by a ".", as not in scope.

Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: LocalVar -> Doc Source #

prettyPrec :: Int -> LocalVar -> Doc Source #

prettyList :: [LocalVar] -> Doc Source #

Pretty NameSpace Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpace -> Doc Source #

prettyPrec :: Int -> NameSpace -> Doc Source #

prettyList :: [NameSpace] -> Doc Source #

Pretty NameSpaceId Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpaceId -> Doc Source #

prettyPrec :: Int -> NameSpaceId -> Doc Source #

prettyList :: [NameSpaceId] -> Doc Source #

Pretty ResolvedName Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ResolvedName -> Doc Source #

prettyPrec :: Int -> ResolvedName -> Doc Source #

prettyList :: [ResolvedName] -> Doc Source #

Pretty Scope Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Scope -> Doc Source #

prettyPrec :: Int -> Scope -> Doc Source #

prettyList :: [Scope] -> Doc Source #

Pretty ScopeInfo Source # 
Instance details

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ScopeInfo -> Doc Source #

prettyPrec :: Int -> ScopeInfo -> Doc Source #

prettyList :: [ScopeInfo] -> Doc Source #

Pretty FlatScope Source # 
Instance details

Defined in Agda.Syntax.Scope.Flat

Methods

pretty :: FlatScope -> Doc Source #

prettyPrec :: Int -> FlatScope -> Doc Source #

prettyList :: [FlatScope] -> Doc Source #

Pretty RawTopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: RawTopLevelModuleName -> Doc Source #

prettyPrec :: Int -> RawTopLevelModuleName -> Doc Source #

prettyList :: [RawTopLevelModuleName] -> Doc Source #

Pretty TopLevelModuleName Source # 
Instance details

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc Source #

prettyPrec :: Int -> TopLevelModuleName -> Doc Source #

prettyList :: [TopLevelModuleName] -> Doc Source #

Pretty TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: TTerm -> Doc Source #

prettyPrec :: Int -> TTerm -> Doc Source #

prettyList :: [TTerm] -> Doc Source #

Pretty CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrix -> Doc Source #

prettyPrec :: Int -> CallMatrix -> Doc Source #

prettyList :: [CallMatrix] -> Doc Source #

Pretty CallPath Source #

Only show intermediate nodes. (Drop last CallInfo).

Instance details

Defined in Agda.Termination.Monad

Methods

pretty :: CallPath -> Doc Source #

prettyPrec :: Int -> CallPath -> Doc Source #

prettyList :: [CallPath] -> Doc Source #

Pretty Order Source # 
Instance details

Defined in Agda.Termination.Order

Methods

pretty :: Order -> Doc Source #

prettyPrec :: Int -> Order -> Doc Source #

prettyList :: [Order] -> Doc Source #

Pretty CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc Source #

prettyPrec :: Int -> CompiledClauses -> Doc Source #

prettyList :: [CompiledClauses] -> Doc Source #

Pretty Cl Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

pretty :: Cl -> Doc Source #

prettyPrec :: Int -> Cl -> Doc Source #

prettyList :: [Cl] -> Doc Source #

Pretty BlockingVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc Source #

prettyPrec :: Int -> BlockingVar -> Doc Source #

prettyList :: [BlockingVar] -> Doc Source #

Pretty SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc Source #

prettyPrec :: Int -> SplitPatVar -> Doc Source #

prettyList :: [SplitPatVar] -> Doc Source #

Pretty SplitTag Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTag -> Doc Source #

prettyPrec :: Int -> SplitTag -> Doc Source #

prettyList :: [SplitTag] -> Doc Source #

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc Source #

prettyPrec :: Int -> Call -> Doc Source #

prettyList :: [Call] -> Doc Source #

Pretty CallInfo Source #

We only show the name of the callee.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CallInfo -> Doc Source #

prettyPrec :: Int -> CallInfo -> Doc Source #

prettyList :: [CallInfo] -> Doc Source #

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CheckpointId -> Doc Source #

prettyPrec :: Int -> CheckpointId -> Doc Source #

prettyList :: [CheckpointId] -> Doc Source #

Pretty CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CompareAs -> Doc Source #

prettyPrec :: Int -> CompareAs -> Doc Source #

prettyList :: [CompareAs] -> Doc Source #

Pretty CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CompareDirection -> Doc Source #

prettyPrec :: Int -> CompareDirection -> Doc Source #

prettyList :: [CompareDirection] -> Doc Source #

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Comparison -> Doc Source #

prettyPrec :: Int -> Comparison -> Doc Source #

prettyList :: [Comparison] -> Doc Source #

Pretty ConstructorData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ConstructorData -> Doc Source #

prettyPrec :: Int -> ConstructorData -> Doc Source #

prettyList :: [ConstructorData] -> Doc Source #

Pretty DataOrRecSigData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DataOrRecSigData -> Doc Source #

prettyPrec :: Int -> DataOrRecSigData -> Doc Source #

prettyList :: [DataOrRecSigData] -> Doc Source #

Pretty DatatypeData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DatatypeData -> Doc Source #

prettyPrec :: Int -> DatatypeData -> Doc Source #

prettyList :: [DatatypeData] -> Doc Source #

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Definition -> Doc Source #

prettyPrec :: Int -> Definition -> Doc Source #

prettyList :: [Definition] -> Doc Source #

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc Source #

prettyPrec :: Int -> Defn -> Doc Source #

prettyList :: [Defn] -> Doc Source #

Pretty DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DisplayForm -> Doc Source #

prettyPrec :: Int -> DisplayForm -> Doc Source #

prettyList :: [DisplayForm] -> Doc Source #

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DisplayTerm -> Doc Source #

prettyPrec :: Int -> DisplayTerm -> Doc Source #

prettyList :: [DisplayTerm] -> Doc Source #

Pretty FunctionData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: FunctionData -> Doc Source #

prettyPrec :: Int -> FunctionData -> Doc Source #

prettyList :: [FunctionData] -> Doc Source #

Pretty Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Interface -> Doc Source #

prettyPrec :: Int -> Interface -> Doc Source #

prettyList :: [Interface] -> Doc Source #

Pretty MetaInstantiation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: MetaInstantiation -> Doc Source #

prettyPrec :: Int -> MetaInstantiation -> Doc Source #

prettyList :: [MetaInstantiation] -> Doc Source #

Pretty NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: NamedMeta -> Doc Source #

prettyPrec :: Int -> NamedMeta -> Doc Source #

prettyList :: [NamedMeta] -> Doc Source #

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Polarity -> Doc Source #

prettyPrec :: Int -> Polarity -> Doc Source #

prettyList :: [Polarity] -> Doc Source #

Pretty PrimitiveData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: PrimitiveData -> Doc Source #

prettyPrec :: Int -> PrimitiveData -> Doc Source #

prettyList :: [PrimitiveData] -> Doc Source #

Pretty PrimitiveSortData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: PrimitiveSortData -> Doc Source #

prettyPrec :: Int -> PrimitiveSortData -> Doc Source #

prettyList :: [PrimitiveSortData] -> Doc Source #

Pretty ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ProjLams -> Doc Source #

prettyPrec :: Int -> ProjLams -> Doc Source #

prettyList :: [ProjLams] -> Doc Source #

Pretty Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Projection -> Doc Source #

prettyPrec :: Int -> Projection -> Doc Source #

prettyList :: [Projection] -> Doc Source #

Pretty ProjectionLikenessMissing Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ProjectionLikenessMissing -> Doc Source #

prettyPrec :: Int -> ProjectionLikenessMissing -> Doc Source #

prettyList :: [ProjectionLikenessMissing] -> Doc Source #

Pretty RecordData Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: RecordData -> Doc Source #

prettyPrec :: Int -> RecordData -> Doc Source #

prettyList :: [RecordData] -> Doc Source #

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Section -> Doc Source #

prettyPrec :: Int -> Section -> Doc Source #

prettyList :: [Section] -> Doc Source #

Pretty TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: TermHead -> Doc Source #

prettyPrec :: Int -> TermHead -> Doc Source #

prettyList :: [TermHead] -> Doc Source #

Pretty DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

pretty :: DeepSizeView -> Doc Source #

prettyPrec :: Int -> DeepSizeView -> Doc Source #

prettyList :: [DeepSizeView] -> Doc Source #

Pretty Item Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Item -> Doc Source #

prettyPrec :: Int -> Item -> Doc Source #

prettyList :: [Item] -> Doc Source #

Pretty Node Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc Source #

prettyPrec :: Int -> Node -> Doc Source #

prettyList :: [Node] -> Doc Source #

Pretty Occurrence Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc Source #

prettyPrec :: Int -> Occurrence -> Doc Source #

prettyList :: [Occurrence] -> Doc Source #

Pretty OccursWhere Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursWhere -> Doc Source #

prettyPrec :: Int -> OccursWhere -> Doc Source #

prettyList :: [OccursWhere] -> Doc Source #

Pretty Where Source # 
Instance details

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc Source #

prettyPrec :: Int -> Where -> Doc Source #

prettyList :: [Where] -> Doc Source #

Pretty Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Lvl -> Doc Source #

prettyPrec :: Int -> Lvl -> Doc Source #

prettyList :: [Lvl] -> Doc Source #

Pretty Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Nat -> Doc Source #

prettyPrec :: Int -> Nat -> Doc Source #

prettyList :: [Nat] -> Doc Source #

Pretty CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

pretty :: CType -> Doc Source #

prettyPrec :: Int -> CType -> Doc Source #

prettyList :: [CType] -> Doc Source #

Pretty AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

pretty :: AsBinding -> Doc Source #

prettyPrec :: Int -> AsBinding -> Doc Source #

prettyList :: [AsBinding] -> Doc Source #

Pretty OldSizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeConstraint -> Doc Source #

prettyPrec :: Int -> OldSizeConstraint -> Doc Source #

prettyList :: [OldSizeConstraint] -> Doc Source #

Pretty OldSizeExpr Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeExpr -> Doc Source #

prettyPrec :: Int -> OldSizeExpr -> Doc Source #

prettyList :: [OldSizeExpr] -> Doc Source #

Pretty NamedRigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: NamedRigid -> Doc Source #

prettyPrec :: Int -> NamedRigid -> Doc Source #

prettyList :: [NamedRigid] -> Doc Source #

Pretty SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: SizeMeta -> Doc Source #

prettyPrec :: Int -> SizeMeta -> Doc Source #

prettyList :: [SizeMeta] -> Doc Source #

Pretty Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Cmp -> Doc Source #

prettyPrec :: Int -> Cmp -> Doc Source #

prettyList :: [Cmp] -> Doc Source #

Pretty Flex Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Flex -> Doc Source #

prettyPrec :: Int -> Flex -> Doc Source #

prettyList :: [Flex] -> Doc Source #

Pretty Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Offset -> Doc Source #

prettyPrec :: Int -> Offset -> Doc Source #

prettyList :: [Offset] -> Doc Source #

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Polarity -> Doc Source #

prettyPrec :: Int -> Polarity -> Doc Source #

prettyList :: [Polarity] -> Doc Source #

Pretty Rigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Rigid -> Doc Source #

prettyPrec :: Int -> Rigid -> Doc Source #

prettyList :: [Rigid] -> Doc Source #

Pretty Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Label -> Doc Source #

prettyPrec :: Int -> Label -> Doc Source #

prettyList :: [Label] -> Doc Source #

Pretty Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Weight -> Doc Source #

prettyPrec :: Int -> Weight -> Doc Source #

prettyList :: [Weight] -> Doc Source #

Pretty CallSite Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: CallSite -> Doc Source #

prettyPrec :: Int -> CallSite -> Doc Source #

prettyList :: [CallSite] -> Doc Source #

Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

pretty :: AbsolutePath -> Doc Source #

prettyPrec :: Int -> AbsolutePath -> Doc Source #

prettyList :: [AbsolutePath] -> Doc Source #

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Alt -> Doc Source #

prettyPrec :: Int -> Alt -> Doc Source #

prettyList :: [Alt] -> Doc Source #

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Binds -> Doc Source #

prettyPrec :: Int -> Binds -> Doc Source #

prettyList :: [Binds] -> Doc Source #

Pretty ConDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ConDecl -> Doc Source #

prettyPrec :: Int -> ConDecl -> Doc Source #

prettyList :: [ConDecl] -> Doc Source #

Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: DataOrNew -> Doc Source #

prettyPrec :: Int -> DataOrNew -> Doc Source #

prettyList :: [DataOrNew] -> Doc Source #

Pretty Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Decl -> Doc Source #

prettyPrec :: Int -> Decl -> Doc Source #

prettyList :: [Decl] -> Doc Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Exp -> Doc Source #

prettyPrec :: Int -> Exp -> Doc Source #

prettyList :: [Exp] -> Doc Source #

Pretty ImportDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportDecl -> Doc Source #

prettyPrec :: Int -> ImportDecl -> Doc Source #

prettyList :: [ImportDecl] -> Doc Source #

Pretty ImportSpec Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportSpec -> Doc Source #

prettyPrec :: Int -> ImportSpec -> Doc Source #

prettyList :: [ImportSpec] -> Doc Source #

Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Literal -> Doc Source #

prettyPrec :: Int -> Literal -> Doc Source #

prettyList :: [Literal] -> Doc Source #

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Match -> Doc Source #

prettyPrec :: Int -> Match -> Doc Source #

prettyList :: [Match] -> Doc Source #

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Module -> Doc Source #

prettyPrec :: Int -> Module -> Doc Source #

prettyList :: [Module] -> Doc Source #

Pretty ModuleName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModuleName -> Doc Source #

prettyPrec :: Int -> ModuleName -> Doc Source #

prettyList :: [ModuleName] -> Doc Source #

Pretty ModulePragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModulePragma -> Doc Source #

prettyPrec :: Int -> ModulePragma -> Doc Source #

prettyList :: [ModulePragma] -> Doc Source #

Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Name -> Doc Source #

prettyPrec :: Int -> Name -> Doc Source #

prettyList :: [Name] -> Doc Source #

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Pat -> Doc Source #

prettyPrec :: Int -> Pat -> Doc Source #

prettyList :: [Pat] -> Doc Source #

Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QName -> Doc Source #

prettyPrec :: Int -> QName -> Doc Source #

prettyList :: [QName] -> Doc Source #

Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QOp -> Doc Source #

prettyPrec :: Int -> QOp -> Doc Source #

prettyList :: [QOp] -> Doc Source #

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Stmt -> Doc Source #

prettyPrec :: Int -> Stmt -> Doc Source #

prettyList :: [Stmt] -> Doc Source #

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Strictness -> Doc Source #

prettyPrec :: Int -> Strictness -> Doc Source #

prettyList :: [Strictness] -> Doc Source #

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: TyVarBind -> Doc Source #

prettyPrec :: Int -> TyVarBind -> Doc Source #

prettyList :: [TyVarBind] -> Doc Source #

Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Type -> Doc Source #

prettyPrec :: Int -> Type -> Doc Source #

prettyList :: [Type] -> Doc Source #

Pretty CPUTime Source #

Print CPU time in milli (10^-3) seconds.

Instance details

Defined in Agda.Utils.Time

Methods

pretty :: CPUTime -> Doc Source #

prettyPrec :: Int -> CPUTime -> Doc Source #

prettyList :: [CPUTime] -> Doc Source #

Pretty Constraint Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: Constraint -> Doc Source #

prettyPrec :: Int -> Constraint -> Doc Source #

prettyList :: [Constraint] -> Doc Source #

Pretty Node Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: Node -> Doc Source #

prettyPrec :: Int -> Node -> Doc Source #

prettyList :: [Node] -> Doc Source #

Pretty SizeExpr Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: SizeExpr -> Doc Source #

prettyPrec :: Int -> SizeExpr -> Doc Source #

prettyList :: [SizeExpr] -> Doc Source #

Pretty Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: Weight -> Doc Source #

prettyPrec :: Int -> Weight -> Doc Source #

prettyList :: [Weight] -> Doc Source #

Pretty Int32 Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Int32 -> Doc Source #

prettyPrec :: Int -> Int32 -> Doc Source #

prettyList :: [Int32] -> Doc Source #

Pretty CallStack Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: CallStack -> Doc Source #

prettyPrec :: Int -> CallStack -> Doc Source #

prettyList :: [CallStack] -> Doc Source #

Pretty SrcLoc Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: SrcLoc -> Doc Source #

prettyPrec :: Int -> SrcLoc -> Doc Source #

prettyList :: [SrcLoc] -> Doc Source #

Pretty Word64 Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Word64 -> Doc Source #

prettyPrec :: Int -> Word64 -> Doc Source #

prettyList :: [Word64] -> Doc Source #

Pretty IntSet Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: IntSet -> Doc Source #

prettyPrec :: Int -> IntSet -> Doc Source #

prettyList :: [IntSet] -> Doc Source #

Pretty Doc Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Doc -> Doc Source #

prettyPrec :: Int -> Doc -> Doc Source #

prettyList :: [Doc] -> Doc Source #

Pretty Text Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Text -> Doc Source #

prettyPrec :: Int -> Text -> Doc Source #

prettyList :: [Text] -> Doc Source #

Pretty Integer Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Integer -> Doc Source #

prettyPrec :: Int -> Integer -> Doc Source #

prettyList :: [Integer] -> Doc Source #

Pretty () Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: () -> Doc Source #

prettyPrec :: Int -> () -> Doc Source #

prettyList :: [()] -> Doc Source #

Pretty Bool Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Bool -> Doc Source #

prettyPrec :: Int -> Bool -> Doc Source #

prettyList :: [Bool] -> Doc Source #

Pretty Char Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Char -> Doc Source #

prettyPrec :: Int -> Char -> Doc Source #

prettyList :: [Char] -> Doc Source #

Pretty Double Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Double -> Doc Source #

prettyPrec :: Int -> Double -> Doc Source #

prettyList :: [Double] -> Doc Source #

Pretty Int Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Int -> Doc Source #

prettyPrec :: Int -> Int -> Doc Source #

prettyList :: [Int] -> Doc Source #

Pretty a => Pretty (Lisp a) Source # 
Instance details

Defined in Agda.Interaction.EmacsCommand

Methods

pretty :: Lisp a -> Doc Source #

prettyPrec :: Int -> Lisp a -> Doc Source #

prettyList :: [Lisp a] -> Doc Source #

Pretty a => Pretty (QNamed a) Source # 
Instance details

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QNamed a -> Doc Source #

prettyPrec :: Int -> QNamed a -> Doc Source #

prettyList :: [QNamed a] -> Doc Source #

Pretty a => Pretty (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc Source #

prettyPrec :: Int -> Arg a -> Doc Source #

prettyList :: [Arg a] -> Doc Source #

Pretty a => Pretty (MaybePlaceholder a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: MaybePlaceholder a -> Doc Source #

prettyPrec :: Int -> MaybePlaceholder a -> Doc Source #

prettyList :: [MaybePlaceholder a] -> Doc Source #

Pretty e => Pretty (Named_ e) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc Source #

prettyPrec :: Int -> Named_ e -> Doc Source #

prettyList :: [Named_ e] -> Doc Source #

Pretty a => Pretty (Ranged a) Source #

Ignores range.

Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc Source #

prettyPrec :: Int -> Ranged a -> Doc Source #

prettyList :: [Ranged a] -> Doc Source #

Pretty a => Pretty (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WithHiding a -> Doc Source #

prettyPrec :: Int -> WithHiding a -> Doc Source #

prettyList :: [WithHiding a] -> Doc Source #

Pretty a => Pretty (WithOrigin a) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: WithOrigin a -> Doc Source #

prettyPrec :: Int -> WithOrigin a -> Doc Source #

prettyList :: [WithOrigin a] -> Doc Source #

Pretty a => Pretty (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Binder' a -> Doc Source #

prettyPrec :: Int -> Binder' a -> Doc Source #

prettyList :: [Binder' a] -> Doc Source #

Pretty a => Pretty (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: FieldAssignment' a -> Doc Source #

prettyPrec :: Int -> FieldAssignment' a -> Doc Source #

prettyList :: [FieldAssignment' a] -> Doc Source #

Pretty (OpApp Expr) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpApp Expr -> Doc Source #

prettyPrec :: Int -> OpApp Expr -> Doc Source #

prettyList :: [OpApp Expr] -> Doc Source #

Pretty (ThingWithFixity Name) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc Source #

prettyPrec :: Int -> ThingWithFixity Name -> Doc Source #

prettyList :: [ThingWithFixity Name] -> Doc Source #

Pretty t => Pretty (Abs t) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc Source #

prettyPrec :: Int -> Abs t -> Doc Source #

prettyList :: [Abs t] -> Doc Source #

Pretty a => Pretty (Blocked a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc Source #

prettyPrec :: Int -> Blocked a -> Doc Source #

prettyList :: [Blocked a] -> Doc Source #

Pretty a => Pretty (Pattern' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Pattern' a -> Doc Source #

prettyPrec :: Int -> Pattern' a -> Doc Source #

prettyList :: [Pattern' a] -> Doc Source #

Pretty a => Pretty (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc Source #

prettyPrec :: Int -> Substitution' a -> Doc Source #

prettyList :: [Substitution' a] -> Doc Source #

Pretty a => Pretty (Tele (Dom a)) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc Source #

prettyPrec :: Int -> Tele (Dom a) -> Doc Source #

prettyList :: [Tele (Dom a)] -> Doc Source #

Pretty tm => Pretty (Elim' tm) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

pretty :: Elim' tm -> Doc Source #

prettyPrec :: Int -> Elim' tm -> Doc Source #

prettyList :: [Elim' tm] -> Doc Source #

Pretty a => Pretty (Interval' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: Interval' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Interval' (Maybe a) -> Doc Source #

prettyList :: [Interval' (Maybe a)] -> Doc Source #

Pretty a => Pretty (Position' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: Position' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Position' (Maybe a) -> Doc Source #

prettyList :: [Position' (Maybe a)] -> Doc Source #

(Pretty a, HasRange a) => Pretty (PrintRange a) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: PrintRange a -> Doc Source #

prettyPrec :: Int -> PrintRange a -> Doc Source #

prettyList :: [PrintRange a] -> Doc Source #

Pretty a => Pretty (Range' (Maybe a)) Source # 
Instance details

Defined in Agda.Syntax.Position

Methods

pretty :: Range' (Maybe a) -> Doc Source #

prettyPrec :: Int -> Range' (Maybe a) -> Doc Source #

prettyList :: [Range' (Maybe a)] -> Doc Source #

Pretty cinfo => Pretty (CallGraph cinfo) Source #

Displays the recursion behaviour corresponding to a call graph.

Instance details

Defined in Agda.Termination.CallGraph

Methods

pretty :: CallGraph cinfo -> Doc Source #

prettyPrec :: Int -> CallGraph cinfo -> Doc Source #

prettyList :: [CallGraph cinfo] -> Doc Source #

Pretty cinfo => Pretty (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CMSet cinfo -> Doc Source #

prettyPrec :: Int -> CMSet cinfo -> Doc Source #

prettyList :: [CMSet cinfo] -> Doc Source #

Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrixAug cinfo -> Doc Source #

prettyPrec :: Int -> CallMatrixAug cinfo -> Doc Source #

prettyList :: [CallMatrixAug cinfo] -> Doc Source #

Pretty a => Pretty (Case a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: Case a -> Doc Source #

prettyPrec :: Int -> Case a -> Doc Source #

prettyList :: [Case a] -> Doc Source #

Pretty a => Pretty (WithArity a) Source # 
Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: WithArity a -> Doc Source #

prettyPrec :: Int -> WithArity a -> Doc Source #

prettyList :: [WithArity a] -> Doc Source #

Pretty a => Pretty (SplitTree' a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTree' a -> Doc Source #

prettyPrec :: Int -> SplitTree' a -> Doc Source #

prettyList :: [SplitTree' a] -> Doc Source #

Pretty a => Pretty (SplitTreeLabel a) Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTreeLabel a -> Doc Source #

prettyPrec :: Int -> SplitTreeLabel a -> Doc Source #

prettyList :: [SplitTreeLabel a] -> Doc Source #

Pretty c => Pretty (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: FunctionInverse' c -> Doc Source #

prettyPrec :: Int -> FunctionInverse' c -> Doc Source #

prettyList :: [FunctionInverse' c] -> Doc Source #

Pretty c => Pretty (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

pretty :: IPBoundary' c -> Doc Source #

prettyPrec :: Int -> IPBoundary' c -> Doc Source #

prettyList :: [IPBoundary' c] -> Doc Source #

Pretty a => Pretty (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Judgement a -> Doc Source #

prettyPrec :: Int -> Judgement a -> Doc Source #

prettyList :: [Judgement a] -> Doc Source #

Pretty a => Pretty (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Open a -> Doc Source #

prettyPrec :: Int -> Open a -> Doc Source #

prettyList :: [Open a] -> Doc Source #

Pretty flex => Pretty (PolarityAssignment flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: PolarityAssignment flex -> Doc Source #

prettyPrec :: Int -> PolarityAssignment flex -> Doc Source #

prettyList :: [PolarityAssignment flex] -> Doc Source #

(Ord a, Pretty a) => Pretty (Benchmark a) Source #

Print benchmark as three-column table with totals.

Instance details

Defined in Agda.Utils.Benchmark

Methods

pretty :: Benchmark a -> Doc Source #

prettyPrec :: Int -> Benchmark a -> Doc Source #

prettyList :: [Benchmark a] -> Doc Source #

Pretty n => Pretty (WithUniqueInt n) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: WithUniqueInt n -> Doc Source #

prettyPrec :: Int -> WithUniqueInt n -> Doc Source #

prettyList :: [WithUniqueInt n] -> Doc Source #

Pretty a => Pretty (List1 a) Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: List1 a -> Doc Source #

prettyPrec :: Int -> List1 a -> Doc Source #

prettyList :: [List1 a] -> Doc Source #

Pretty a => Pretty (IntMap a) Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: IntMap a -> Doc Source #

prettyPrec :: Int -> IntMap a -> Doc Source #

prettyList :: [IntMap a] -> Doc Source #

Pretty a => Pretty (Set a) Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Set a -> Doc Source #

prettyPrec :: Int -> Set a -> Doc Source #

prettyList :: [Set a] -> Doc Source #

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

Defined in Agda.Utils.Pretty

Methods

pretty :: Maybe a -> Doc Source #

prettyPrec :: Int -> Maybe a -> Doc Source #

prettyList :: [Maybe a] -> Doc Source #

Pretty a => Pretty [a] Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: [a] -> Doc Source #

prettyPrec :: Int -> [a] -> Doc Source #

prettyList :: [[a]] -> Doc Source #

(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint a b -> Doc Source #

prettyPrec :: Int -> OutputConstraint a b -> Doc Source #

prettyList :: [OutputConstraint a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint' a b -> Doc Source #

prettyPrec :: Int -> OutputConstraint' a b -> Doc Source #

prettyList :: [OutputConstraint' a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputForm a b -> Doc Source #

prettyPrec :: Int -> OutputForm a b -> Doc Source #

prettyList :: [OutputForm a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportDirective' a b -> Doc Source #

prettyPrec :: Int -> ImportDirective' a b -> Doc Source #

prettyList :: [ImportDirective' a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportedName' a b -> Doc Source #

prettyPrec :: Int -> ImportedName' a b -> Doc Source #

prettyList :: [ImportedName' a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (Renaming' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Renaming' a b -> Doc Source #

prettyPrec :: Int -> Renaming' a b -> Doc Source #

prettyList :: [Renaming' a b] -> Doc Source #

(Pretty a, Pretty b) => Pretty (Using' a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc Source #

prettyPrec :: Int -> Using' a b -> Doc Source #

prettyList :: [Using' a b] -> Doc Source #

(Pretty t, Pretty e) => Pretty (Dom' t e) Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc Source #

prettyPrec :: Int -> Dom' t e -> Doc Source #

prettyList :: [Dom' t e] -> Doc Source #

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b) Source # 
Instance details

Defined in Agda.Termination.SparseMatrix

Methods

pretty :: Matrix i b -> Doc Source #

prettyPrec :: Int -> Matrix i b -> Doc Source #

prettyList :: [Matrix i b] -> Doc Source #

(Pretty r, Pretty f) => Pretty (Constraint' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Constraint' r f -> Doc Source #

prettyPrec :: Int -> Constraint' r f -> Doc Source #

prettyList :: [Constraint' r f] -> Doc Source #

(Pretty r, Pretty f) => Pretty (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: SizeExpr' r f -> Doc Source #

prettyPrec :: Int -> SizeExpr' r f -> Doc Source #

prettyList :: [SizeExpr' r f] -> Doc Source #

(Pretty r, Pretty f) => Pretty (Solution r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Solution r f -> Doc Source #

prettyPrec :: Int -> Solution r f -> Doc Source #

prettyList :: [Solution r f] -> Doc Source #

(Pretty rigid, Pretty flex) => Pretty (Node rigid flex) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Node rigid flex -> Doc Source #

prettyPrec :: Int -> Node rigid flex -> Doc Source #

prettyList :: [Node rigid flex] -> Doc Source #

(Pretty n, Pretty e) => Pretty (Edge n e) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Edge n e -> Doc Source #

prettyPrec :: Int -> Edge n e -> Doc Source #

prettyList :: [Edge n e] -> Doc Source #

(Ord n, Pretty n, Pretty e) => Pretty (Graph n e) Source # 
Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Graph n e -> Doc Source #

prettyPrec :: Int -> Graph n e -> Doc Source #

prettyList :: [Graph n e] -> Doc Source #

(Pretty a, Pretty b) => Pretty (Either a b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Either a b -> Doc Source #

prettyPrec :: Int -> Either a b -> Doc Source #

prettyList :: [Either a b] -> Doc Source #

(Pretty k, Pretty v) => Pretty (Map k v) Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Map k v -> Doc Source #

prettyPrec :: Int -> Map k v -> Doc Source #

prettyList :: [Map k v] -> Doc Source #

(Pretty a, Pretty b) => Pretty (a, b) Source # 
Instance details

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: (a, b) -> Doc Source #

prettyPrec :: Int -> (a, b) -> Doc Source #

prettyList :: [(a, b)] -> Doc Source #

(Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) Source # 
Instance details

Defined in Agda.Utils.Warshall

Methods

pretty :: LegendMatrix a b c -> Doc Source #

prettyPrec :: Int -> LegendMatrix a b c -> Doc Source #

prettyList :: [LegendMatrix a b c] -> Doc Source #

(Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn nm p e -> Doc Source #

prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source #

prettyList :: [RewriteEqn' qn nm p e] -> Doc Source #

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

a ? b = hang a 2 b

hcat :: Foldable t => t Doc -> Doc Source #

hsep :: Foldable t => t Doc -> Doc Source #

vcat :: Foldable t => t Doc -> Doc Source #

punctuate :: Foldable t => Doc -> t Doc -> [Doc] Source #

sep :: Foldable t => t Doc -> Doc Source #

fsep :: Foldable t => t Doc -> Doc Source #

prettyShow :: Pretty a => a -> String Source #

Use instead of show when printing to world.

prettyList_ :: Pretty a => [a] -> Doc Source #

Comma separated list, without the brackets.

mparens :: Bool -> Doc -> Doc Source #

Apply parens to Doc if boolean is true.

pshow :: Show a => a -> Doc Source #

pshow = text . show

prettySet :: Pretty a => [a] -> Doc Source #

Pretty print a set.

prettyMap :: (Pretty k, Pretty v) => [(k, v)] -> Doc Source #

Pretty print an association list.

pwords :: String -> [Doc] Source #

fwords :: String -> Doc Source #

hsepWith :: Doc -> Doc -> Doc -> Doc Source #

Separate, but only if both separees are not null.

prettyAssign :: (Pretty k, Pretty v) => (k, v) -> Doc Source #

Pretty print a single association.

parensNonEmpty :: Doc -> Doc Source #

Only wrap in parens if not empty

align :: Int -> [(String, Doc)] -> Doc Source #

align max rows lays out the elements of rows in two columns, with the second components aligned. The alignment column of the second components is at most max characters to the right of the left-most column.

Precondition: max > 0.

multiLineText :: String -> Doc Source #

Handles strings with newlines properly (preserving indentation)

singPlural :: Sized a => a -> c -> c -> c Source #

prefixedThings :: Doc -> [Doc] -> Doc Source #

Used for with-like telescopes

data Mode #

Rendering mode.

Constructors

PageMode

Normal rendering (lineLength and ribbonsPerLine respected').

ZigZagMode

With zig-zag cuts.

LeftMode

No indentation, infinitely long lines (lineLength ignored), but explicit new lines, i.e., text "one" $$ text "two", are respected.

OneLineMode

All on one line, lineLength ignored and explicit new lines ($$) are turned into spaces.

Instances

Instances details
Generic Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Mode :: Type -> Type #

Methods

from :: Mode -> Rep Mode x #

to :: Rep Mode x -> Mode #

Show Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Mode -> ShowS #

show :: Mode -> String #

showList :: [Mode] -> ShowS #

Eq Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Mode -> Mode -> Bool #

(/=) :: Mode -> Mode -> Bool #

type Rep Mode 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

type Rep Mode = D1 ('MetaData "Mode" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) ((C1 ('MetaCons "PageMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ZigZagMode" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LeftMode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OneLineMode" 'PrefixI 'False) (U1 :: Type -> Type)))

data Style #

A rendering style. Allows us to specify constraints to choose among the many different rendering options.

Constructors

Style 

Fields

  • mode :: Mode

    The rendering mode.

  • lineLength :: Int

    Maximum length of a line, in characters.

  • ribbonsPerLine :: Float

    Ratio of line length to ribbon length. A ribbon refers to the characters on a line excluding indentation. So a lineLength of 100, with a ribbonsPerLine of 2.0 would only allow up to 50 characters of ribbon to be displayed on a line, while allowing it to be indented up to 50 characters.

Instances

Instances details
Generic Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Style :: Type -> Type #

Methods

from :: Style -> Rep Style x #

to :: Rep Style x -> Style #

Show Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Style -> ShowS #

show :: Style -> String #

showList :: [Style] -> ShowS #

Eq Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Style -> Style -> Bool #

(/=) :: Style -> Style -> Bool #

type Rep Style 
Instance details

Defined in Text.PrettyPrint.Annotated.HughesPJ

type Rep Style = D1 ('MetaData "Style" "Text.PrettyPrint.Annotated.HughesPJ" "pretty-1.1.3.6" 'False) (C1 ('MetaCons "Style" 'PrefixI 'True) (S1 ('MetaSel ('Just "mode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Mode) :*: (S1 ('MetaSel ('Just "lineLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "ribbonsPerLine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Float))))

data Doc #

The abstract type of documents. A Doc represents a set of layouts. A Doc with no occurrences of Union or NoDoc represents just one layout.

Instances

Instances details
EncodeTCM Doc Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value Source #

Underscore Doc Source # 
Instance details

Defined in Agda.Syntax.Common

Methods

underscore :: Doc Source #

isUnderscore :: Doc -> Bool Source #

ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #

TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #

EmbPrj Doc Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32 Source #

icod_ :: Doc -> S Int32 Source #

value :: Int32 -> R Doc Source #

Null Doc Source # 
Instance details

Defined in Agda.Utils.Null

Methods

empty :: Doc Source #

null :: Doc -> Bool Source #

Pretty Doc Source # 
Instance details

Defined in Agda.Utils.Pretty

Methods

pretty :: Doc -> Doc Source #

prettyPrec :: Int -> Doc -> Doc Source #

prettyList :: [Doc] -> Doc Source #

ToJSON Doc Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value #

toEncoding :: Doc -> Encoding #

toJSONList :: [Doc] -> Value #

toEncodingList :: [Doc] -> Encoding #

IsString Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

fromString :: String -> Doc #

Monoid Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

mempty :: Doc #

mappend :: Doc -> Doc -> Doc #

mconcat :: [Doc] -> Doc #

Semigroup Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

(<>) :: Doc -> Doc -> Doc #

sconcat :: NonEmpty Doc -> Doc #

stimes :: Integral b => b -> Doc -> Doc #

Generic Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Associated Types

type Rep Doc :: Type -> Type #

Methods

from :: Doc -> Rep Doc x #

to :: Rep Doc x -> Doc #

Show Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

showsPrec :: Int -> Doc -> ShowS #

show :: Doc -> String #

showList :: [Doc] -> ShowS #

NFData Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

rnf :: Doc -> () #

Eq Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

Methods

(==) :: Doc -> Doc -> Bool #

(/=) :: Doc -> Doc -> Bool #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #

Null (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc Source #

null :: AbsToCon Doc -> Bool Source #

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

IsString (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc #

Semigroup (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc #

sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc #

stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc #

Semigroup (TCM Doc) Source #

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc #

stimes :: Integral b => b -> TCM Doc -> TCM Doc #

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc Source #

null :: PureConversionT m Doc -> Bool Source #

type Rep Doc 
Instance details

Defined in Text.PrettyPrint.HughesPJ

type Rep Doc = D1 ('MetaData "Doc" "Text.PrettyPrint.HughesPJ" "pretty-1.1.3.6" 'True) (C1 ('MetaCons "Doc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Doc ()))))

pattern Chr :: !Char -> TextDetails #

A single Char fragment

pattern PStr :: String -> TextDetails #

Used to represent a Fast String fragment but now deprecated and identical to the Str constructor.

text :: String -> Doc #

A document of height 1 containing a literal string. text satisfies the following laws:

The side condition on the last law is necessary because text "" has height 1, while empty has no height.

char :: Char -> Doc #

A document of height and width 1, containing a literal character.

parens #

Arguments

:: Doc 
-> Doc

Wrap document in (...)

(<+>) :: Doc -> Doc -> Doc infixl 6 #

Beside, separated by space, unless one of the arguments is empty. <+> is associative, with identity empty.

isEmpty :: Doc -> Bool #

Returns True if the document is empty

space #

Arguments

:: Doc

A space character

integer #

Arguments

:: Integer 
-> Doc
integer n = text (show n)

float #

Arguments

:: Float 
-> Doc
float n = text (show n)

braces #

Arguments

:: Doc 
-> Doc

Wrap document in {...}

brackets #

Arguments

:: Doc 
-> Doc

Wrap document in [...]

semi #

Arguments

:: Doc

A ';' character

comma #

Arguments

:: Doc

A ',' character

colon #

Arguments

:: Doc

A : character

ptext :: String -> Doc #

Same as text. Used to be used for Bytestrings.

sizedText :: Int -> String -> Doc #

Some text with any width. (text s = sizedText (length s) s)

zeroWidthText :: String -> Doc #

Some text, but without any width. Use for non-printing text such as a HTML or Latex tags

equals #

Arguments

:: Doc

A '=' character

lparen #

Arguments

:: Doc

A '(' character

rparen #

Arguments

:: Doc

A ')' character

lbrack #

Arguments

:: Doc

A '[' character

rbrack #

Arguments

:: Doc

A ']' character

lbrace #

Arguments

:: Doc

A '{' character

rbrace #

Arguments

:: Doc

A '}' character

int #

Arguments

:: Int 
-> Doc
int n = text (show n)

double #

Arguments

:: Double 
-> Doc
double n = text (show n)

rational #

Arguments

:: Rational 
-> Doc
rational n = text (show n)

quotes #

Arguments

:: Doc 
-> Doc

Wrap document in '...'

doubleQuotes #

Arguments

:: Doc 
-> Doc

Wrap document in "..."

nest :: Int -> Doc -> Doc #

Nest (or indent) a document by a given number of positions (which may also be negative). nest satisfies the laws:

The side condition on the last law is needed because empty is a left identity for <>.

hang :: Doc -> Int -> Doc -> Doc #

hang d1 n d2 = sep [d1, nest n d2]

($$) :: Doc -> Doc -> Doc infixl 5 #

Above, except that if the last line of the first argument stops at least one position before the first line of the second begins, these two lines are overlapped. For example:

   text "hi" $$ nest 5 (text "there")

lays out as

   hi   there

rather than

   hi
        there

$$ is associative, with identity empty, and also satisfies

  • (x $$ y) <> z = x $$ (y <> z), if y non-empty.

($+$) :: Doc -> Doc -> Doc infixl 5 #

Above, with no overlapping. $+$ is associative, with identity empty.

cat :: [Doc] -> Doc #

Either hcat or vcat.

fcat :: [Doc] -> Doc #

"Paragraph fill" version of cat.

style :: Style #

The default style (mode=PageMode, lineLength=100, ribbonsPerLine=1.5).

render :: Doc -> String #

Render the Doc to a String using the default Style (see style).

renderStyle :: Style -> Doc -> String #

Render the Doc to a String using the given Style.

fullRender #

Arguments

:: Mode

Rendering mode.

-> Int

Line length.

-> Float

Ribbons per line.

-> (TextDetails -> a -> a)

What to do with text.

-> a

What to do at the end.

-> Doc

The document.

-> a

Result.

The general rendering interface. Please refer to the Style and Mode types for a description of rendering mode, line length and ribbons.

(<>) :: Semigroup a => a -> a -> a infixr 6 #

An associative operation.

>>> [1,2,3] <> [4,5,6]
[1,2,3,4,5,6]