Agda.Utils.Pretty

Pretty printing functions.

Documentation

class Pretty a where

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

prettyPrec :: Int -> a -> Doc

prettyList :: [a] -> Doc

Instances

Pretty Bool

Defined in Agda.Utils.Pretty

Methods

pretty :: Bool -> Doc

prettyPrec :: Int -> Bool -> Doc

prettyList :: [Bool] -> Doc

Pretty Char

Defined in Agda.Utils.Pretty

Methods

pretty :: Char -> Doc

prettyPrec :: Int -> Char -> Doc

prettyList :: [Char] -> Doc

Pretty Int

Defined in Agda.Utils.Pretty

Methods

pretty :: Int -> Doc

prettyPrec :: Int -> Int -> Doc

prettyList :: [Int] -> Doc

Pretty Int32

Defined in Agda.Utils.Pretty

Methods

pretty :: Int32 -> Doc

prettyPrec :: Int -> Int32 -> Doc

prettyList :: [Int32] -> Doc

Pretty Integer

Defined in Agda.Utils.Pretty

Methods

pretty :: Integer -> Doc

prettyPrec :: Int -> Integer -> Doc

prettyList :: [Integer] -> Doc

Pretty ()

Defined in Agda.Utils.Pretty

Methods

pretty :: () -> Doc

prettyPrec :: Int -> () -> Doc

prettyList :: [()] -> Doc

Pretty Doc

Defined in Agda.Utils.Pretty

Methods

pretty :: Doc -> Doc

prettyPrec :: Int -> Doc -> Doc

prettyList :: [Doc] -> Doc

Pretty TyVarBind

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: TyVarBind -> Doc

prettyPrec :: Int -> TyVarBind -> Doc

prettyList :: [TyVarBind] -> Doc

Pretty QOp

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QOp -> Doc

prettyPrec :: Int -> QOp -> Doc

prettyList :: [QOp] -> Doc

Pretty Name

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty QName

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty ModuleName

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

Pretty Literal

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

Pretty Alt

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Alt -> Doc

prettyPrec :: Int -> Alt -> Doc

prettyList :: [Alt] -> Doc

Pretty Exp

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Exp -> Doc

prettyPrec :: Int -> Exp -> Doc

prettyList :: [Exp] -> Doc

Pretty Stmt

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Stmt -> Doc

prettyPrec :: Int -> Stmt -> Doc

prettyList :: [Stmt] -> Doc

Pretty Pat

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Pat -> Doc

prettyPrec :: Int -> Pat -> Doc

prettyList :: [Pat] -> Doc

Pretty Type

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty Match

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Match -> Doc

prettyPrec :: Int -> Match -> Doc

prettyList :: [Match] -> Doc

Pretty Binds

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Binds -> Doc

prettyPrec :: Int -> Binds -> Doc

prettyList :: [Binds] -> Doc

Pretty Strictness

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Strictness -> Doc

prettyPrec :: Int -> Strictness -> Doc

prettyList :: [Strictness] -> Doc

Pretty ConDecl

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ConDecl -> Doc

prettyPrec :: Int -> ConDecl -> Doc

prettyList :: [ConDecl] -> Doc

Pretty DataOrNew

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: DataOrNew -> Doc

prettyPrec :: Int -> DataOrNew -> Doc

prettyList :: [DataOrNew] -> Doc

Pretty Decl

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Decl -> Doc

prettyPrec :: Int -> Decl -> Doc

prettyList :: [Decl] -> Doc

Pretty ImportSpec

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportSpec -> Doc

prettyPrec :: Int -> ImportSpec -> Doc

prettyList :: [ImportSpec] -> Doc

Pretty ImportDecl

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportDecl -> Doc

prettyPrec :: Int -> ImportDecl -> Doc

prettyList :: [ImportDecl] -> Doc

Pretty ModulePragma

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModulePragma -> Doc

prettyPrec :: Int -> ModulePragma -> Doc

prettyList :: [ModulePragma] -> Doc

Pretty Module

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Module -> Doc

prettyPrec :: Int -> Module -> Doc

prettyList :: [Module] -> Doc

Pretty AbsolutePath

Defined in Agda.Utils.FileName

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

prettyList :: [AbsolutePath] -> Doc

Pretty Polarity

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty Cmp

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Cmp -> Doc

prettyPrec :: Int -> Cmp -> Doc

prettyList :: [Cmp] -> Doc

Pretty Flex

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Flex -> Doc

prettyPrec :: Int -> Flex -> Doc

prettyList :: [Flex] -> Doc

Pretty Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Rigid -> Doc

prettyPrec :: Int -> Rigid -> Doc

prettyList :: [Rigid] -> Doc

Pretty Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Offset -> Doc

prettyPrec :: Int -> Offset -> Doc

prettyList :: [Offset] -> Doc

Pretty CPUTime

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

Defined in Agda.Utils.Time

Methods

pretty :: CPUTime -> Doc

prettyPrec :: Int -> CPUTime -> Doc

prettyList :: [CPUTime] -> Doc

Pretty IntervalWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

prettyList :: [IntervalWithoutFile] -> Doc

Pretty PositionWithoutFile

Defined in Agda.Syntax.Position

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

prettyList :: [PositionWithoutFile] -> Doc

Pretty GenPart

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: GenPart -> Doc

prettyPrec :: Int -> GenPart -> Doc

prettyList :: [GenPart] -> Doc

Pretty Fixity'

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity' -> Doc

prettyPrec :: Int -> Fixity' -> Doc

prettyList :: [Fixity'] -> Doc

Pretty Fixity

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Fixity -> Doc

prettyPrec :: Int -> Fixity -> Doc

prettyList :: [Fixity] -> Doc

Pretty InteractionId

Defined in Agda.Syntax.Common

Methods

pretty :: InteractionId -> Doc

prettyPrec :: Int -> InteractionId -> Doc

prettyList :: [InteractionId] -> Doc

Pretty MetaId

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

Pretty NameId

Defined in Agda.Syntax.Common

Methods

pretty :: NameId -> Doc

prettyPrec :: Int -> NameId -> Doc

prettyList :: [NameId] -> Doc

Pretty Access

Defined in Agda.Syntax.Common

Methods

pretty :: Access -> Doc

prettyPrec :: Int -> Access -> Doc

prettyList :: [Access] -> Doc

Pretty Cohesion

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Cohesion -> Doc

prettyPrec :: Int -> Cohesion -> Doc

prettyList :: [Cohesion] -> Doc

Pretty Relevance

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

Pretty Quantity

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Quantity -> Doc

prettyPrec :: Int -> Quantity -> Doc

prettyList :: [Quantity] -> Doc

Pretty QωOrigin

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: QωOrigin -> Doc

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

prettyList :: [QωOrigin] -> Doc

Pretty Q1Origin

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q1Origin -> Doc

prettyPrec :: Int -> Q1Origin -> Doc

prettyList :: [Q1Origin] -> Doc

Pretty Q0Origin

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q0Origin -> Doc

prettyPrec :: Int -> Q0Origin -> Doc

prettyList :: [Q0Origin] -> Doc

Pretty Hiding

Defined in Agda.Syntax.Common

Methods

pretty :: Hiding -> Doc

prettyPrec :: Int -> Hiding -> Doc

prettyList :: [Hiding] -> Doc

Pretty Induction

Defined in Agda.Syntax.Common

Methods

pretty :: Induction -> Doc

prettyPrec :: Int -> Induction -> Doc

prettyList :: [Induction] -> Doc

Pretty FileType

Defined in Agda.Syntax.Common

Methods

pretty :: FileType -> Doc

prettyPrec :: Int -> FileType -> Doc

prettyList :: [FileType] -> Doc

Pretty TopLevelModuleName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

prettyList :: [TopLevelModuleName] -> Doc

Pretty QName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

Pretty Name

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty Polarity

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty ProblemId

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

prettyList :: [ProblemId] -> Doc

Pretty Comparison

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> Comparison -> Doc

prettyList :: [Comparison] -> Doc

Pretty NamedMeta

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: NamedMeta -> Doc

prettyPrec :: Int -> NamedMeta -> Doc

prettyList :: [NamedMeta] -> Doc

Pretty ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

Pretty ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

Pretty AmbiguousQName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: AmbiguousQName -> Doc

prettyPrec :: Int -> AmbiguousQName -> Doc

prettyList :: [AmbiguousQName] -> Doc

Pretty ModuleName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

Pretty QName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty Name

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty Precedence

Defined in Agda.Syntax.Fixity

Methods

pretty :: Precedence -> Doc

prettyPrec :: Int -> Precedence -> Doc

prettyList :: [Precedence] -> Doc

Pretty Literal

Defined in Agda.Syntax.Literal

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

Pretty TTerm

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: TTerm -> Doc

prettyPrec :: Int -> TTerm -> Doc

prettyList :: [TTerm] -> Doc

Pretty LibWarning'

Defined in Agda.Interaction.Library

Methods

pretty :: LibWarning' -> Doc

prettyPrec :: Int -> LibWarning' -> Doc

prettyList :: [LibWarning'] -> Doc

Pretty Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Label -> Doc

prettyPrec :: Int -> Label -> Doc

prettyList :: [Label] -> Doc

Pretty Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Weight -> Doc

prettyPrec :: Int -> Weight -> Doc

prettyList :: [Weight] -> Doc

Pretty Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc

prettyPrec :: Int -> Occurrence -> Doc

prettyList :: [Occurrence] -> Doc

Pretty Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc

prettyPrec :: Int -> Where -> Doc

prettyList :: [Where] -> Doc

Pretty OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursWhere -> Doc

prettyPrec :: Int -> OccursWhere -> Doc

prettyList :: [OccursWhere] -> Doc

Pretty Pragma

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

Pretty OpenShortHand

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

Pretty ModuleApplication

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

Pretty Declaration

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Declaration -> Doc

prettyPrec :: Int -> Declaration -> Doc

prettyList :: [Declaration] -> Doc

Pretty LamClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

Pretty WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

Pretty RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

Pretty LHSCore

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHSCore -> Doc

prettyPrec :: Int -> LHSCore -> Doc

prettyList :: [LHSCore] -> Doc

Pretty LHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

Pretty TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

Pretty BoundName

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty DoStmt

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

Pretty Pattern

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

Pretty Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

Pretty ModuleAssignment

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

Pretty Tel

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

prettyList :: [Tel] -> Doc

Pretty NamedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NamedBinding -> Doc

prettyPrec :: Int -> NamedBinding -> Doc

prettyList :: [NamedBinding] -> Doc

Pretty SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTag -> Doc

prettyPrec :: Int -> SplitTag -> Doc

prettyList :: [SplitTag] -> Doc

Pretty Phase

Defined in Agda.Benchmarking

Methods

pretty :: Phase -> Doc

prettyPrec :: Int -> Phase -> Doc

prettyList :: [Phase] -> Doc

Pretty ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ResolvedName -> Doc

prettyPrec :: Int -> ResolvedName -> Doc

prettyList :: [ResolvedName] -> Doc

Pretty AbstractModule

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractModule -> Doc

prettyPrec :: Int -> AbstractModule -> Doc

prettyList :: [AbstractModule] -> Doc

Pretty AbstractName

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: AbstractName -> Doc

prettyPrec :: Int -> AbstractName -> Doc

prettyList :: [AbstractName] -> Doc

Pretty NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpace -> Doc

prettyPrec :: Int -> NameSpace -> Doc

prettyList :: [NameSpace] -> Doc

Pretty LocalVar

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

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: LocalVar -> Doc

prettyPrec :: Int -> LocalVar -> Doc

prettyList :: [LocalVar] -> Doc

Pretty ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ScopeInfo -> Doc

prettyPrec :: Int -> ScopeInfo -> Doc

prettyList :: [ScopeInfo] -> Doc

Pretty NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpaceId -> Doc

prettyPrec :: Int -> NameSpaceId -> Doc

prettyList :: [NameSpaceId] -> Doc

Pretty Scope

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Scope -> Doc

prettyPrec :: Int -> Scope -> Doc

prettyList :: [Scope] -> Doc

Pretty Order

Defined in Agda.Termination.Order

Methods

pretty :: Order -> Doc

prettyPrec :: Int -> Order -> Doc

prettyList :: [Order] -> Doc

Pretty CallMatrix

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

prettyList :: [CallMatrix] -> Doc

Pretty DBPatVar

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

prettyList :: [DBPatVar] -> Doc

Pretty Clause

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

Pretty LevelAtom

Defined in Agda.Syntax.Internal

Methods

pretty :: LevelAtom -> Doc

prettyPrec :: Int -> LevelAtom -> Doc

prettyList :: [LevelAtom] -> Doc

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty Term

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty ConHead

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

Pretty ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

prettyList :: [ScopeCopyInfo] -> Doc

Pretty DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

Pretty DeclarationException

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: DeclarationException -> Doc

prettyPrec :: Int -> DeclarationException -> Doc

prettyList :: [DeclarationException] -> Doc

Pretty NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions

Methods

pretty :: NiceDeclaration -> Doc

prettyPrec :: Int -> NiceDeclaration -> Doc

prettyList :: [NiceDeclaration] -> Doc

Pretty LibWarning

Defined in Agda.Interaction.Library

Methods

pretty :: LibWarning -> Doc

prettyPrec :: Int -> LibWarning -> Doc

prettyList :: [LibWarning] -> Doc

Pretty CallInfo

We only show the name of the callee.

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CallInfo -> Doc

prettyPrec :: Int -> CallInfo -> Doc

prettyList :: [CallInfo] -> Doc

Pretty Call

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> Call -> Doc

prettyList :: [Call] -> Doc

Pretty TermHead

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: TermHead -> Doc

prettyPrec :: Int -> TermHead -> Doc

prettyList :: [TermHead] -> Doc

Pretty Defn

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc

prettyPrec :: Int -> Defn -> Doc

prettyList :: [Defn] -> Doc

Pretty Definition

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Definition -> Doc

prettyPrec :: Int -> Definition -> Doc

prettyList :: [Definition] -> Doc

Pretty DisplayTerm

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DisplayTerm -> Doc

prettyPrec :: Int -> DisplayTerm -> Doc

prettyList :: [DisplayTerm] -> Doc

Pretty Section

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Section -> Doc

prettyPrec :: Int -> Section -> Doc

prettyList :: [Section] -> Doc

Pretty CompareDirection

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CompareDirection -> Doc

prettyPrec :: Int -> CompareDirection -> Doc

prettyList :: [CompareDirection] -> Doc

Pretty Interface

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> Interface -> Doc

prettyList :: [Interface] -> Doc

Pretty CheckpointId

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CheckpointId -> Doc

prettyPrec :: Int -> CheckpointId -> Doc

prettyList :: [CheckpointId] -> Doc

Pretty DeepSizeView

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

pretty :: DeepSizeView -> Doc

prettyPrec :: Int -> DeepSizeView -> Doc

prettyList :: [DeepSizeView] -> Doc

Pretty OldSizeConstraint

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeConstraint -> Doc

prettyPrec :: Int -> OldSizeConstraint -> Doc

prettyList :: [OldSizeConstraint] -> Doc

Pretty OldSizeExpr

Defined in Agda.TypeChecking.SizedTypes

Methods

pretty :: OldSizeExpr -> Doc

prettyPrec :: Int -> OldSizeExpr -> Doc

prettyList :: [OldSizeExpr] -> Doc

Pretty AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

prettyList :: [AsBinding] -> Doc

Pretty Node

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc

prettyPrec :: Int -> Node -> Doc

prettyList :: [Node] -> Doc

Pretty SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc

prettyPrec :: Int -> SplitPatVar -> Doc

prettyList :: [SplitPatVar] -> Doc

Pretty BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

Pretty CallPath

Only show intermediate nodes. (Drop last CallInfo).

Defined in Agda.Termination.Monad

Methods

pretty :: CallPath -> Doc

prettyPrec :: Int -> CallPath -> Doc

prettyList :: [CallPath] -> Doc

Pretty SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: SizeMeta -> Doc

prettyPrec :: Int -> SizeMeta -> Doc

prettyList :: [SizeMeta] -> Doc

Pretty NamedRigid

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: NamedRigid -> Doc

prettyPrec :: Int -> NamedRigid -> Doc

prettyList :: [NamedRigid] -> Doc

Pretty Cl

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

pretty :: Cl -> Doc

prettyPrec :: Int -> Cl -> Doc

prettyList :: [Cl] -> Doc

Pretty HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

pretty :: HaskellPragma -> Doc

prettyPrec :: Int -> HaskellPragma -> Doc

prettyList :: [HaskellPragma] -> Doc

Pretty a => Pretty [a]

Defined in Agda.Utils.Pretty

Methods

pretty :: [a] -> Doc

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

prettyList :: [[a]] -> Doc

Pretty a => Pretty (Maybe a)

Defined in Agda.Utils.Pretty

Methods

pretty :: Maybe a -> Doc

prettyPrec :: Int -> Maybe a -> Doc

prettyList :: [Maybe a] -> Doc

Pretty a => Pretty (NonEmpty a)

Defined in Agda.Utils.Pretty

Methods

pretty :: NonEmpty a -> Doc

prettyPrec :: Int -> NonEmpty a -> Doc

prettyList :: [NonEmpty a] -> Doc

Pretty flex => Pretty (PolarityAssignment flex)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: PolarityAssignment flex -> Doc

prettyPrec :: Int -> PolarityAssignment flex -> Doc

prettyList :: [PolarityAssignment flex] -> Doc

Pretty a => Pretty (Lisp a)

Defined in Agda.Interaction.EmacsCommand

Methods

pretty :: Lisp a -> Doc

prettyPrec :: Int -> Lisp a -> Doc

prettyList :: [Lisp a] -> Doc

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

Print benchmark as three-column table with totals.

Defined in Agda.Utils.Benchmark

Methods

pretty :: Benchmark a -> Doc

prettyPrec :: Int -> Benchmark a -> Doc

prettyList :: [Benchmark a] -> Doc

(Pretty a, HasRange a) => Pretty (PrintRange a)

Defined in Agda.Syntax.Position

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

prettyList :: [PrintRange a] -> Doc

Pretty a => Pretty (Range' (Maybe a))

Defined in Agda.Syntax.Position

Methods

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

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

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

Pretty a => Pretty (Interval' (Maybe a))

Defined in Agda.Syntax.Position

Methods

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

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

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

Pretty a => Pretty (Position' (Maybe a))

Defined in Agda.Syntax.Position

Methods

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

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

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

Pretty a => Pretty (MaybePlaceholder a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: MaybePlaceholder a -> Doc

prettyPrec :: Int -> MaybePlaceholder a -> Doc

prettyList :: [MaybePlaceholder a] -> Doc

Pretty a => Pretty (Ranged a)

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc

prettyPrec :: Int -> Ranged a -> Doc

prettyList :: [Ranged a] -> Doc

Pretty e => Pretty (Named_ e)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Named_ e -> Doc

prettyPrec :: Int -> Named_ e -> Doc

prettyList :: [Named_ e] -> Doc

Pretty a => Pretty (Arg a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Arg a -> Doc

prettyPrec :: Int -> Arg a -> Doc

prettyList :: [Arg a] -> Doc

Pretty a => Pretty (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

pretty :: WithOrigin a -> Doc

prettyPrec :: Int -> WithOrigin a -> Doc

prettyList :: [WithOrigin a] -> Doc

Pretty a => Pretty (WithHiding a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WithHiding a -> Doc

prettyPrec :: Int -> WithHiding a -> Doc

prettyList :: [WithHiding a] -> Doc

Pretty a => Pretty (QNamed a)

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QNamed a -> Doc

prettyPrec :: Int -> QNamed a -> Doc

prettyList :: [QNamed a] -> Doc

Pretty (ThingWithFixity Name)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ThingWithFixity Name -> Doc

prettyPrec :: Int -> ThingWithFixity Name -> Doc

prettyList :: [ThingWithFixity Name] -> Doc

Pretty a => Pretty (Binder' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Binder' a -> Doc

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

prettyList :: [Binder' a] -> Doc

Pretty a => Pretty (FieldAssignment' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: FieldAssignment' a -> Doc

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

prettyList :: [FieldAssignment' a] -> Doc

Pretty (OpApp Expr)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpApp Expr -> Doc

prettyPrec :: Int -> OpApp Expr -> Doc

prettyList :: [OpApp Expr] -> Doc

Pretty a => Pretty (SplitTreeLabel a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTreeLabel a -> Doc

prettyPrec :: Int -> SplitTreeLabel a -> Doc

prettyList :: [SplitTreeLabel a] -> Doc

Pretty a => Pretty (SplitTree' a)

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTree' a -> Doc

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

prettyList :: [SplitTree' a] -> Doc

Pretty cinfo => Pretty (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CMSet cinfo -> Doc

prettyPrec :: Int -> CMSet cinfo -> Doc

prettyList :: [CMSet cinfo] -> Doc

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrixAug cinfo -> Doc

prettyPrec :: Int -> CallMatrixAug cinfo -> Doc

prettyList :: [CallMatrixAug cinfo] -> Doc

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

Defined in Agda.Termination.CallGraph

Methods

pretty :: CallGraph cinfo -> Doc

prettyPrec :: Int -> CallGraph cinfo -> Doc

prettyList :: [CallGraph cinfo] -> Doc

Pretty a => Pretty (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' a] -> Doc

Pretty a => Pretty (Pattern' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Pattern' a -> Doc

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

prettyList :: [Pattern' a] -> Doc

Pretty a => Pretty (Tele (Dom a))

Defined in Agda.Syntax.Internal

Methods

pretty :: Tele (Dom a) -> Doc

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

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

Pretty tm => Pretty (Elim' tm)

Defined in Agda.Syntax.Internal

Methods

pretty :: Elim' tm -> Doc

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

prettyList :: [Elim' tm] -> Doc

Pretty a => Pretty (Case a)

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: Case a -> Doc

prettyPrec :: Int -> Case a -> Doc

prettyList :: [Case a] -> Doc

Pretty a => Pretty (WithArity a)

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: WithArity a -> Doc

prettyPrec :: Int -> WithArity a -> Doc

prettyList :: [WithArity a] -> Doc

Pretty c => Pretty (IPBoundary' c)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: IPBoundary' c -> Doc

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

prettyList :: [IPBoundary' c] -> Doc

(Pretty a, Pretty b) => Pretty (Either a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Either a b -> Doc

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

prettyList :: [Either a b] -> Doc

(Pretty a, Pretty b) => Pretty (a, b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: (a, b) -> Doc

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

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

(Pretty r, Pretty f) => Pretty (Solution r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Solution r f -> Doc

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

prettyList :: [Solution r f] -> Doc

(Pretty r, Pretty f) => Pretty (Constraint' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Constraint' r f -> Doc

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

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

(Pretty r, Pretty f) => Pretty (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: SizeExpr' r f -> Doc

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

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

(Pretty a, Pretty b) => Pretty (Renaming' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Renaming' a b -> Doc

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

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

(Pretty a, Pretty b) => Pretty (ImportedName' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportedName' a b -> Doc

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

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

(Pretty a, Pretty b) => Pretty (Using' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Using' a b -> Doc

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

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

(Pretty a, Pretty b) => Pretty (ImportDirective' a b)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ImportDirective' a b -> Doc

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

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

(Pretty n, Pretty e) => Pretty (Edge n e)

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Edge n e -> Doc

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

prettyList :: [Edge n e] -> Doc

(Ord n, Pretty n, Pretty e) => Pretty (Graph n e)

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: Graph n e -> Doc

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

prettyList :: [Graph n e] -> Doc

(Pretty rigid, Pretty flex) => Pretty (Node rigid flex)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Node rigid flex -> Doc

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

prettyList :: [Node rigid flex] -> Doc

(Integral i, HasZero b, Pretty b) => Pretty (Matrix i b)

Defined in Agda.Termination.SparseMatrix

Methods

pretty :: Matrix i b -> Doc

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

prettyList :: [Matrix i b] -> Doc

(Pretty t, Pretty e) => Pretty (Dom' t e)

Defined in Agda.Syntax.Internal

Methods

pretty :: Dom' t e -> Doc

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

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

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint' a b -> Doc

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

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

(Pretty a, Pretty b) => Pretty (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint a b -> Doc

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

prettyList :: [OutputConstraint a b] -> Doc

(Pretty a, Pretty b) => Pretty (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputForm a b -> Doc

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

prettyList :: [OutputForm a b] -> Doc

(Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e)

Defined in Agda.Syntax.Common

Methods

pretty :: RewriteEqn' qn p e -> Doc

prettyPrec :: Int -> RewriteEqn' qn p e -> Doc

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

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

pwords :: String -> [Doc]

fwords :: String -> Doc

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

Comma separated list, without the brackets.

mparens :: Bool -> Doc -> Doc

Apply parens to Doc if boolean is true.

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

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

Handles strings with newlines properly (preserving indentation)

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

a ? b = hang a 2 b

pshow :: Show a => a -> Doc

pshow = text . pretty

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

prefixedThings :: Doc -> [Doc] -> Doc

Used for with-like telescopes

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.

renderStyle :: Style -> Doc -> String

Render the Doc to a String using the given Style.

render :: Doc -> String

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

fsep :: [Doc] -> Doc

"Paragraph fill" version of sep.

fcat :: [Doc] -> Doc

"Paragraph fill" version of cat.

cat :: [Doc] -> Doc

Either hcat or vcat.

sep :: [Doc] -> Doc

Either hsep or vcat.

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

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

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

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

($$) :: 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.

punctuate :: Doc -> [Doc] -> [Doc]

punctuate p [d1, ... dn] = [d1 <> p, d2 <> p, ... dn-1 <> p, dn]

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

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

nest :: Int -> Doc -> Doc

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

• nest 0 x = x

• nest k (nest k' x) = nest (k+k') x

• nest k (x <> y) = nest k x <> nest k y

• nest k (x $$ y) = nest k x $$ nest k y

• nest k empty = empty

• x <> nest k y = x <> y, if x non-empty

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

vcat :: [Doc] -> Doc

List version of $$.

hsep :: [Doc] -> Doc

List version of <+>.

hcat :: [Doc] -> Doc

List version of <>.

braces

Arguments

:: Doc

-> Doc

Wrap document in {...}

brackets

Arguments

:: Doc

-> Doc

Wrap document in [...]

parens

Arguments

:: Doc

-> Doc

Wrap document in (...)

doubleQuotes

Arguments

:: Doc

-> Doc

Wrap document in "..."

quotes

Arguments

:: Doc

-> Doc

Wrap document in '...'

rational

Arguments

:: Rational

-> Doc

rational n = text (show n)

double

Arguments

:: Double

-> Doc

double n = text (show n)

float

Arguments

:: Float

-> Doc

float n = text (show n)

integer

Arguments

:: Integer

-> Doc

integer n = text (show n)

int

Arguments

:: Int

-> Doc

int n = text (show n)

rbrace

Arguments

:: Doc

A '}' character

lbrace

Arguments

:: Doc

A '{' character

rbrack

Arguments

:: Doc

A ']' character

lbrack

Arguments

:: Doc

A '[' character

rparen

Arguments

:: Doc

A ')' character

lparen

Arguments

:: Doc

A '(' character

equals

Arguments

:: Doc

A '=' character

space

Arguments

:: Doc

A space character

colon

Arguments

:: Doc

A : character

comma

Arguments

:: Doc

A ',' character

semi

Arguments

:: Doc

A ';' character

isEmpty :: Doc -> Bool

Returns True if the document is empty

zeroWidthText :: String -> Doc

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

sizedText :: Int -> String -> Doc

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

ptext :: String -> Doc

Same as text. Used to be used for Bytestrings.

text :: String -> Doc

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

• text s <> text t = text (s++t)

• text "" <> x = x, if x non-empty

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.

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

Eq Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

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

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

Data Doc

Defined in Agda.Utils.Pretty

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc

toConstr :: Doc -> Constr

dataTypeOf :: Doc -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc)

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc

Show Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

showsPrec :: Int -> Doc -> ShowS

show :: Doc -> String

showList :: [Doc] -> ShowS

IsString Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

fromString :: String -> Doc

Generic Doc

Defined in Text.PrettyPrint.HughesPJ

Associated Types

type Rep Doc :: Type -> Type

Methods

from :: Doc -> Rep Doc x

to :: Rep Doc x -> Doc

Semigroup Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

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

sconcat :: NonEmpty Doc -> Doc

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

Monoid Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

mempty :: Doc

mappend :: Doc -> Doc -> Doc

mconcat :: [Doc] -> Doc

ToJSON Doc

Defined in Agda.Interaction.JSON

Methods

toJSON :: Doc -> Value

toEncoding :: Doc -> Encoding

toJSONList :: [Doc] -> Value

toEncodingList :: [Doc] -> Encoding

NFData Doc

Defined in Text.PrettyPrint.HughesPJ

Methods

rnf :: Doc -> ()

Null Doc

Defined in Agda.Utils.Null

Methods

empty :: Doc

null :: Doc -> Bool

Pretty Doc

Defined in Agda.Utils.Pretty

Methods

pretty :: Doc -> Doc

prettyPrec :: Int -> Doc -> Doc

prettyList :: [Doc] -> Doc

Underscore Doc

Defined in Agda.Syntax.Common

Methods

underscore :: Doc

isUnderscore :: Doc -> Bool

EmbPrj Doc

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Doc -> S Int32

icod_ :: Doc -> S Int32

value :: Int32 -> R Doc

TraceS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

EncodeTCM Doc

Defined in Agda.Interaction.JSON

Methods

encodeTCM :: Doc -> TCM Value

Semigroup (TCM Doc)

Defined in Agda.TypeChecking.Warnings

Methods

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

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

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

Null (TCM Doc)

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

TraceS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

Monad m => Null (PureConversionT m Doc)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

empty :: PureConversionT m Doc

null :: PureConversionT m Doc -> Bool

Monad m => Semigroup (StateT s m Doc)

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: StateT s m Doc -> StateT s m Doc -> StateT s m Doc

sconcat :: NonEmpty (StateT s m Doc) -> StateT s m Doc

stimes :: Integral b => b -> StateT s m Doc -> StateT s m Doc

Applicative m => Semigroup (ReaderT s m Doc)

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: ReaderT s m Doc -> ReaderT s m Doc -> ReaderT s m Doc

sconcat :: NonEmpty (ReaderT s m Doc) -> ReaderT s m Doc

stimes :: Integral b => b -> ReaderT s m Doc -> ReaderT s m Doc

type Rep Doc

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 ()))))

style :: Style

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

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.

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

Eq Style

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

Show Style

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Style -> ShowS

show :: Style -> String

showList :: [Style] -> ShowS

Generic Style

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Style :: Type -> Type

Methods

from :: Style -> Rep Style x

to :: Rep Style x -> Style

type Rep Style

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

Eq Mode

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

Show Mode

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

Generic Mode

Defined in Text.PrettyPrint.Annotated.HughesPJ

Associated Types

type Rep Mode :: Type -> Type

Methods

from :: Mode -> Rep Mode x

to :: Rep Mode x -> Mode

type Rep Mode

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)))

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

An associative operation.

Orphan instances

Data Doc

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Doc -> c Doc

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Doc

toConstr :: Doc -> Constr

dataTypeOf :: Doc -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Doc)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Doc)

gmapT :: (forall b. Data b => b -> b) -> Doc -> Doc

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Doc -> r

gmapQ :: (forall d. Data d => d -> u) -> Doc -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Doc -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Doc -> m Doc

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Doc -> m Doc