Agda.Syntax.Common.Pretty

Pretty printing functions.

Documentation

type Doc = Doc Aspects

The type of documents. We use documents annotated by Aspects to record syntactic highlighting information that is generated during pretty-printing.

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 Phase

Defined in Agda.Benchmarking

Methods

pretty :: Phase -> Doc

prettyPrec :: Int -> Phase -> Doc

prettyList :: [Phase] -> Doc

Pretty HaskellPragma

Defined in Agda.Compiler.MAlonzo.Pragmas

Methods

pretty :: HaskellPragma -> Doc

prettyPrec :: Int -> HaskellPragma -> Doc

prettyList :: [HaskellPragma] -> Doc

Pretty CompilerBackend

Defined in Agda.Interaction.Base

Methods

pretty :: CompilerBackend -> Doc

prettyPrec :: Int -> CompilerBackend -> Doc

prettyList :: [CompilerBackend] -> Doc

Pretty InterfaceFile

Defined in Agda.Interaction.FindFile

Methods

pretty :: InterfaceFile -> Doc

prettyPrec :: Int -> InterfaceFile -> Doc

prettyList :: [InterfaceFile] -> Doc

Pretty SourceFile

Defined in Agda.Interaction.FindFile

Methods

pretty :: SourceFile -> Doc

prettyPrec :: Int -> SourceFile -> Doc

prettyList :: [SourceFile] -> Doc

Pretty LibError'

Pretty-print library management error without position info.

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibError' -> Doc

prettyPrec :: Int -> LibError' -> Doc

prettyList :: [LibError'] -> Doc

Pretty LibParseError

Print library file parse error without position info.

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibParseError -> Doc

prettyPrec :: Int -> LibParseError -> Doc

prettyList :: [LibParseError] -> Doc

Pretty LibWarning

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning -> Doc

prettyPrec :: Int -> LibWarning -> Doc

prettyList :: [LibWarning] -> Doc

Pretty LibWarning'

Defined in Agda.Interaction.Library.Base

Methods

pretty :: LibWarning' -> Doc

prettyPrec :: Int -> LibWarning' -> Doc

prettyList :: [LibWarning'] -> Doc

Pretty OptionWarning

Defined in Agda.Interaction.Options.Base

Methods

pretty :: OptionWarning -> Doc

prettyPrec :: Int -> OptionWarning -> Doc

prettyList :: [OptionWarning] -> Doc

Pretty HintMode

Defined in Agda.Mimer.Options

Methods

pretty :: HintMode -> Doc

prettyPrec :: Int -> HintMode -> Doc

prettyList :: [HintMode] -> Doc

Pretty ScopeCopyInfo

Defined in Agda.Syntax.Abstract

Methods

pretty :: ScopeCopyInfo -> Doc

prettyPrec :: Int -> ScopeCopyInfo -> Doc

prettyList :: [ScopeCopyInfo] -> 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 Name

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty QName

Defined in Agda.Syntax.Abstract.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty Suffix

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Suffix -> Doc

prettyPrec :: Int -> Suffix -> Doc

prettyList :: [Suffix] -> Doc

Pretty BuiltinId

Defined in Agda.Syntax.Builtin

Methods

pretty :: BuiltinId -> Doc

prettyPrec :: Int -> BuiltinId -> Doc

prettyList :: [BuiltinId] -> Doc

Pretty PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

pretty :: PrimitiveId -> Doc

prettyPrec :: Int -> PrimitiveId -> Doc

prettyList :: [PrimitiveId] -> Doc

Pretty Access

Defined in Agda.Syntax.Common

Methods

pretty :: Access -> Doc

prettyPrec :: Int -> Access -> Doc

prettyList :: [Access] -> Doc

Pretty Associativity

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Associativity -> Doc

prettyPrec :: Int -> Associativity -> Doc

prettyList :: [Associativity] -> Doc

Pretty Cohesion

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Cohesion -> Doc

prettyPrec :: Int -> Cohesion -> Doc

prettyList :: [Cohesion] -> Doc

Pretty Erased

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Erased -> Doc

prettyPrec :: Int -> Erased -> Doc

prettyList :: [Erased] -> Doc

Pretty FileType

Defined in Agda.Syntax.Common

Methods

pretty :: FileType -> Doc

prettyPrec :: Int -> FileType -> Doc

prettyList :: [FileType] -> 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 FixityLevel

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: FixityLevel -> Doc

prettyPrec :: Int -> FixityLevel -> Doc

prettyList :: [FixityLevel] -> Doc

Pretty Hiding

Defined in Agda.Syntax.Common

Methods

pretty :: Hiding -> Doc

prettyPrec :: Int -> Hiding -> Doc

prettyList :: [Hiding] -> Doc

Pretty InteractionId

Defined in Agda.Syntax.Common

Methods

pretty :: InteractionId -> Doc

prettyPrec :: Int -> InteractionId -> Doc

prettyList :: [InteractionId] -> Doc

Pretty Lock

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Lock -> Doc

prettyPrec :: Int -> Lock -> Doc

prettyList :: [Lock] -> Doc

Pretty MetaId

Defined in Agda.Syntax.Common

Methods

pretty :: MetaId -> Doc

prettyPrec :: Int -> MetaId -> Doc

prettyList :: [MetaId] -> Doc

Pretty Modality

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Modality -> Doc

prettyPrec :: Int -> Modality -> Doc

prettyList :: [Modality] -> Doc

Pretty NameId

Defined in Agda.Syntax.Common

Methods

pretty :: NameId -> Doc

prettyPrec :: Int -> NameId -> Doc

prettyList :: [NameId] -> Doc

Pretty NotationPart

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NotationPart -> Doc

prettyPrec :: Int -> NotationPart -> Doc

prettyList :: [NotationPart] -> Doc

Pretty OpaqueId

Defined in Agda.Syntax.Common

Methods

pretty :: OpaqueId -> Doc

prettyPrec :: Int -> OpaqueId -> Doc

prettyList :: [OpaqueId] -> Doc

Pretty OverlapMode

Defined in Agda.Syntax.Common

Methods

pretty :: OverlapMode -> Doc

prettyPrec :: Int -> OverlapMode -> Doc

prettyList :: [OverlapMode] -> Doc

Pretty ProblemId

Defined in Agda.Syntax.Common

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

prettyList :: [ProblemId] -> Doc

Pretty Q0Origin

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q0Origin -> Doc

prettyPrec :: Int -> Q0Origin -> Doc

prettyList :: [Q0Origin] -> Doc

Pretty Q1Origin

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Q1Origin -> Doc

prettyPrec :: Int -> Q1Origin -> Doc

prettyList :: [Q1Origin] -> 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 Relevance

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Relevance -> Doc

prettyPrec :: Int -> Relevance -> Doc

prettyList :: [Relevance] -> Doc

Pretty Induction

Defined in Agda.Syntax.Common

Methods

pretty :: Induction -> Doc

prettyPrec :: Int -> Induction -> Doc

prettyList :: [Induction] -> Doc

Pretty KwRange

Defined in Agda.Syntax.Common.KeywordRange

Methods

pretty :: KwRange -> Doc

prettyPrec :: Int -> KwRange -> Doc

prettyList :: [KwRange] -> Doc

Pretty BoundName

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: BoundName -> Doc

prettyPrec :: Int -> BoundName -> Doc

prettyList :: [BoundName] -> Doc

Pretty Declaration

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Declaration -> Doc

prettyPrec :: Int -> Declaration -> Doc

prettyList :: [Declaration] -> Doc

Pretty DoStmt

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: DoStmt -> Doc

prettyPrec :: Int -> DoStmt -> Doc

prettyList :: [DoStmt] -> Doc

Pretty Expr

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Expr -> Doc

prettyPrec :: Int -> Expr -> Doc

prettyList :: [Expr] -> Doc

Pretty LHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHS -> Doc

prettyPrec :: Int -> LHS -> Doc

prettyList :: [LHS] -> Doc

Pretty LHSCore

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LHSCore -> Doc

prettyPrec :: Int -> LHSCore -> Doc

prettyList :: [LHSCore] -> Doc

Pretty LamBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamBinding -> Doc

prettyPrec :: Int -> LamBinding -> Doc

prettyList :: [LamBinding] -> Doc

Pretty LamClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: LamClause -> Doc

prettyPrec :: Int -> LamClause -> Doc

prettyList :: [LamClause] -> Doc

Pretty ModuleApplication

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleApplication -> Doc

prettyPrec :: Int -> ModuleApplication -> Doc

prettyList :: [ModuleApplication] -> Doc

Pretty ModuleAssignment

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: ModuleAssignment -> Doc

prettyPrec :: Int -> ModuleAssignment -> Doc

prettyList :: [ModuleAssignment] -> Doc

Pretty OpenShortHand

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: OpenShortHand -> Doc

prettyPrec :: Int -> OpenShortHand -> Doc

prettyList :: [OpenShortHand] -> Doc

Pretty Pattern

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pattern -> Doc

prettyPrec :: Int -> Pattern -> Doc

prettyList :: [Pattern] -> Doc

Pretty Pragma

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Pragma -> Doc

prettyPrec :: Int -> Pragma -> Doc

prettyList :: [Pragma] -> Doc

Pretty RHS

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RHS -> Doc

prettyPrec :: Int -> RHS -> Doc

prettyList :: [RHS] -> Doc

Pretty RecordDirective

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: RecordDirective -> Doc

prettyPrec :: Int -> RecordDirective -> Doc

prettyList :: [RecordDirective] -> Doc

Pretty TypedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TypedBinding -> Doc

prettyPrec :: Int -> TypedBinding -> Doc

prettyList :: [TypedBinding] -> Doc

Pretty WhereClause

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: WhereClause -> Doc

prettyPrec :: Int -> WhereClause -> Doc

prettyList :: [WhereClause] -> Doc

Pretty DeclarationException'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationException' -> Doc

prettyPrec :: Int -> DeclarationException' -> Doc

prettyList :: [DeclarationException'] -> Doc

Pretty DeclarationWarning

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning -> Doc

prettyPrec :: Int -> DeclarationWarning -> Doc

prettyList :: [DeclarationWarning] -> Doc

Pretty DeclarationWarning'

Defined in Agda.Syntax.Concrete.Definitions.Errors

Methods

pretty :: DeclarationWarning' -> Doc

prettyPrec :: Int -> DeclarationWarning' -> Doc

prettyList :: [DeclarationWarning'] -> Doc

Pretty DataRecOrFun

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

pretty :: DataRecOrFun -> Doc

prettyPrec :: Int -> DataRecOrFun -> Doc

prettyList :: [DataRecOrFun] -> Doc

Pretty NiceDeclaration

Defined in Agda.Syntax.Concrete.Definitions.Types

Methods

pretty :: NiceDeclaration -> Doc

prettyPrec :: Int -> NiceDeclaration -> Doc

prettyList :: [NiceDeclaration] -> Doc

Pretty Name

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty NamePart

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: NamePart -> Doc

prettyPrec :: Int -> NamePart -> Doc

prettyList :: [NamePart] -> Doc

Pretty QName

Defined in Agda.Syntax.Concrete.Name

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty NamedBinding

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: NamedBinding -> Doc

prettyPrec :: Int -> NamedBinding -> Doc

prettyList :: [NamedBinding] -> Doc

Pretty Tel

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: Tel -> Doc

prettyPrec :: Int -> Tel -> Doc

prettyList :: [Tel] -> Doc

Pretty Precedence

Defined in Agda.Syntax.Fixity

Methods

pretty :: Precedence -> Doc

prettyPrec :: Int -> Precedence -> Doc

prettyList :: [Precedence] -> Doc

Pretty Clause

Defined in Agda.Syntax.Internal

Methods

pretty :: Clause -> Doc

prettyPrec :: Int -> Clause -> Doc

prettyList :: [Clause] -> Doc

Pretty ConHead

Defined in Agda.Syntax.Internal

Methods

pretty :: ConHead -> Doc

prettyPrec :: Int -> ConHead -> Doc

prettyList :: [ConHead] -> Doc

Pretty DBPatVar

Defined in Agda.Syntax.Internal

Methods

pretty :: DBPatVar -> Doc

prettyPrec :: Int -> DBPatVar -> Doc

prettyList :: [DBPatVar] -> Doc

Pretty Level

Defined in Agda.Syntax.Internal

Methods

pretty :: Level -> Doc

prettyPrec :: Int -> Level -> Doc

prettyList :: [Level] -> Doc

Pretty PlusLevel

Defined in Agda.Syntax.Internal

Methods

pretty :: PlusLevel -> Doc

prettyPrec :: Int -> PlusLevel -> Doc

prettyList :: [PlusLevel] -> Doc

Pretty Sort

Defined in Agda.Syntax.Internal

Methods

pretty :: Sort -> Doc

prettyPrec :: Int -> Sort -> Doc

prettyList :: [Sort] -> Doc

Pretty Term

Defined in Agda.Syntax.Internal

Methods

pretty :: Term -> Doc

prettyPrec :: Int -> Term -> Doc

prettyList :: [Term] -> Doc

Pretty Type

Defined in Agda.Syntax.Internal

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> Doc

Pretty Blocker

Defined in Agda.Syntax.Internal.Blockers

Methods

pretty :: Blocker -> Doc

prettyPrec :: Int -> Blocker -> Doc

prettyList :: [Blocker] -> Doc

Pretty Literal

Defined in Agda.Syntax.Literal

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

Pretty NewNotation

Defined in Agda.Syntax.Notation

Methods

pretty :: NewNotation -> Doc

prettyPrec :: Int -> NewNotation -> Doc

prettyList :: [NewNotation] -> Doc

Pretty NotationKind

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationKind -> Doc

prettyPrec :: Int -> NotationKind -> Doc

prettyList :: [NotationKind] -> Doc

Pretty NotationSection

Defined in Agda.Syntax.Notation

Methods

pretty :: NotationSection -> Doc

prettyPrec :: Int -> NotationSection -> Doc

prettyList :: [NotationSection] -> Doc

Pretty ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

Pretty ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

Pretty IntervalWithoutFile

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntervalWithoutFile -> Doc

prettyPrec :: Int -> IntervalWithoutFile -> Doc

prettyList :: [IntervalWithoutFile] -> Doc

Pretty PositionWithoutFile

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: PositionWithoutFile -> Doc

prettyPrec :: Int -> PositionWithoutFile -> Doc

prettyList :: [PositionWithoutFile] -> Doc

Pretty RangeFile

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: RangeFile -> Doc

prettyPrec :: Int -> RangeFile -> Doc

prettyList :: [RangeFile] -> 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 BindingSource

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: BindingSource -> Doc

prettyPrec :: Int -> BindingSource -> Doc

prettyList :: [BindingSource] -> 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 NameSpace

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpace -> Doc

prettyPrec :: Int -> NameSpace -> Doc

prettyList :: [NameSpace] -> Doc

Pretty NameSpaceId

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: NameSpaceId -> Doc

prettyPrec :: Int -> NameSpaceId -> Doc

prettyList :: [NameSpaceId] -> Doc

Pretty ResolvedName

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ResolvedName -> Doc

prettyPrec :: Int -> ResolvedName -> Doc

prettyList :: [ResolvedName] -> Doc

Pretty Scope

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: Scope -> Doc

prettyPrec :: Int -> Scope -> Doc

prettyList :: [Scope] -> Doc

Pretty ScopeInfo

Defined in Agda.Syntax.Scope.Base

Methods

pretty :: ScopeInfo -> Doc

prettyPrec :: Int -> ScopeInfo -> Doc

prettyList :: [ScopeInfo] -> Doc

Pretty FlatScope

Defined in Agda.Syntax.Scope.Flat

Methods

pretty :: FlatScope -> Doc

prettyPrec :: Int -> FlatScope -> Doc

prettyList :: [FlatScope] -> Doc

Pretty RawTopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: RawTopLevelModuleName -> Doc

prettyPrec :: Int -> RawTopLevelModuleName -> Doc

prettyList :: [RawTopLevelModuleName] -> Doc

Pretty TopLevelModuleName

Defined in Agda.Syntax.TopLevelModuleName

Methods

pretty :: TopLevelModuleName -> Doc

prettyPrec :: Int -> TopLevelModuleName -> Doc

prettyList :: [TopLevelModuleName] -> Doc

Pretty Compiled

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: Compiled -> Doc

prettyPrec :: Int -> Compiled -> Doc

prettyList :: [Compiled] -> Doc

Pretty TTerm

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: TTerm -> Doc

prettyPrec :: Int -> TTerm -> Doc

prettyList :: [TTerm] -> Doc

Pretty CallMatrix

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

prettyList :: [CallMatrix] -> 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 Order

Defined in Agda.Termination.Order

Methods

pretty :: Order -> Doc

prettyPrec :: Int -> Order -> Doc

prettyList :: [Order] -> Doc

Pretty CompiledClauses

Defined in Agda.TypeChecking.CompiledClause

Methods

pretty :: CompiledClauses -> Doc

prettyPrec :: Int -> CompiledClauses -> Doc

prettyList :: [CompiledClauses] -> Doc

Pretty Cl

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

pretty :: Cl -> Doc

prettyPrec :: Int -> Cl -> Doc

prettyList :: [Cl] -> Doc

Pretty BlockingVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: BlockingVar -> Doc

prettyPrec :: Int -> BlockingVar -> Doc

prettyList :: [BlockingVar] -> Doc

Pretty SplitPatVar

Defined in Agda.TypeChecking.Coverage.Match

Methods

pretty :: SplitPatVar -> Doc

prettyPrec :: Int -> SplitPatVar -> Doc

prettyList :: [SplitPatVar] -> Doc

Pretty SplitTag

Defined in Agda.TypeChecking.Coverage.SplitTree

Methods

pretty :: SplitTag -> Doc

prettyPrec :: Int -> SplitTag -> Doc

prettyList :: [SplitTag] -> Doc

Pretty Call

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> Call -> Doc

prettyList :: [Call] -> 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 CheckpointId

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CheckpointId -> Doc

prettyPrec :: Int -> CheckpointId -> Doc

prettyList :: [CheckpointId] -> Doc

Pretty CompareAs

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CompareAs -> Doc

prettyPrec :: Int -> CompareAs -> Doc

prettyList :: [CompareAs] -> Doc

Pretty CompareDirection

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: CompareDirection -> Doc

prettyPrec :: Int -> CompareDirection -> Doc

prettyList :: [CompareDirection] -> Doc

Pretty Comparison

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> Comparison -> Doc

prettyList :: [Comparison] -> Doc

Pretty ConstructorData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ConstructorData -> Doc

prettyPrec :: Int -> ConstructorData -> Doc

prettyList :: [ConstructorData] -> Doc

Pretty DataOrRecSigData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DataOrRecSigData -> Doc

prettyPrec :: Int -> DataOrRecSigData -> Doc

prettyList :: [DataOrRecSigData] -> Doc

Pretty DatatypeData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DatatypeData -> Doc

prettyPrec :: Int -> DatatypeData -> Doc

prettyList :: [DatatypeData] -> Doc

Pretty Definition

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Definition -> Doc

prettyPrec :: Int -> Definition -> Doc

prettyList :: [Definition] -> Doc

Pretty Defn

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc

prettyPrec :: Int -> Defn -> Doc

prettyList :: [Defn] -> Doc

Pretty DisplayForm

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DisplayForm -> Doc

prettyPrec :: Int -> DisplayForm -> Doc

prettyList :: [DisplayForm] -> Doc

Pretty DisplayTerm

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: DisplayTerm -> Doc

prettyPrec :: Int -> DisplayTerm -> Doc

prettyList :: [DisplayTerm] -> Doc

Pretty FunctionData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: FunctionData -> Doc

prettyPrec :: Int -> FunctionData -> Doc

prettyList :: [FunctionData] -> Doc

Pretty Interface

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> Interface -> Doc

prettyList :: [Interface] -> Doc

Pretty MetaInstantiation

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: MetaInstantiation -> Doc

prettyPrec :: Int -> MetaInstantiation -> Doc

prettyList :: [MetaInstantiation] -> Doc

Pretty NamedMeta

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: NamedMeta -> Doc

prettyPrec :: Int -> NamedMeta -> Doc

prettyList :: [NamedMeta] -> Doc

Pretty OpaqueBlock

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: OpaqueBlock -> Doc

prettyPrec :: Int -> OpaqueBlock -> Doc

prettyList :: [OpaqueBlock] -> Doc

Pretty Polarity

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty PrimitiveData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: PrimitiveData -> Doc

prettyPrec :: Int -> PrimitiveData -> Doc

prettyList :: [PrimitiveData] -> Doc

Pretty PrimitiveSortData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: PrimitiveSortData -> Doc

prettyPrec :: Int -> PrimitiveSortData -> Doc

prettyList :: [PrimitiveSortData] -> Doc

Pretty ProjLams

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ProjLams -> Doc

prettyPrec :: Int -> ProjLams -> Doc

prettyList :: [ProjLams] -> Doc

Pretty Projection

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Projection -> Doc

prettyPrec :: Int -> Projection -> Doc

prettyList :: [Projection] -> Doc

Pretty ProjectionLikenessMissing

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ProjectionLikenessMissing -> Doc

prettyPrec :: Int -> ProjectionLikenessMissing -> Doc

prettyList :: [ProjectionLikenessMissing] -> Doc

Pretty RecordData

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: RecordData -> Doc

prettyPrec :: Int -> RecordData -> Doc

prettyList :: [RecordData] -> Doc

Pretty Section

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Section -> Doc

prettyPrec :: Int -> Section -> Doc

prettyList :: [Section] -> Doc

Pretty TermHead

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: TermHead -> Doc

prettyPrec :: Int -> TermHead -> Doc

prettyList :: [TermHead] -> Doc

Pretty DeepSizeView

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

pretty :: DeepSizeView -> Doc

prettyPrec :: Int -> DeepSizeView -> Doc

prettyList :: [DeepSizeView] -> Doc

Pretty Item

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Item -> Doc

prettyPrec :: Int -> Item -> Doc

prettyList :: [Item] -> Doc

Pretty Node

Defined in Agda.TypeChecking.Positivity

Methods

pretty :: Node -> Doc

prettyPrec :: Int -> Node -> Doc

prettyList :: [Node] -> Doc

Pretty Occurrence

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Occurrence -> Doc

prettyPrec :: Int -> Occurrence -> Doc

prettyList :: [Occurrence] -> Doc

Pretty OccursWhere

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: OccursWhere -> Doc

prettyPrec :: Int -> OccursWhere -> Doc

prettyList :: [OccursWhere] -> Doc

Pretty Where

Defined in Agda.TypeChecking.Positivity.Occurrence

Methods

pretty :: Where -> Doc

prettyPrec :: Int -> Where -> Doc

prettyList :: [Where] -> Doc

Pretty Lvl

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Lvl -> Doc

prettyPrec :: Int -> Lvl -> Doc

prettyList :: [Lvl] -> Doc

Pretty Nat

Defined in Agda.TypeChecking.Primitive

Methods

pretty :: Nat -> Doc

prettyPrec :: Int -> Nat -> Doc

prettyList :: [Nat] -> Doc

Pretty CType

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

pretty :: CType -> Doc

prettyPrec :: Int -> CType -> Doc

prettyList :: [CType] -> Doc

Pretty AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

prettyList :: [AsBinding] -> 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 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 NamedRigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: NamedRigid -> Doc

prettyPrec :: Int -> NamedRigid -> Doc

prettyList :: [NamedRigid] -> Doc

Pretty Offset

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Offset -> Doc

prettyPrec :: Int -> Offset -> Doc

prettyList :: [Offset] -> Doc

Pretty Polarity

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

Pretty Rigid

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: Rigid -> Doc

prettyPrec :: Int -> Rigid -> Doc

prettyList :: [Rigid] -> Doc

Pretty SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

pretty :: SizeMeta -> Doc

prettyPrec :: Int -> SizeMeta -> Doc

prettyList :: [SizeMeta] -> 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 CallSite

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: CallSite -> Doc

prettyPrec :: Int -> CallSite -> Doc

prettyList :: [CallSite] -> Doc

Pretty AbsolutePath

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: AbsolutePath -> Doc

prettyPrec :: Int -> AbsolutePath -> Doc

prettyList :: [AbsolutePath] -> Doc

Pretty Alt

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Alt -> Doc

prettyPrec :: Int -> Alt -> Doc

prettyList :: [Alt] -> Doc

Pretty Binds

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Binds -> Doc

prettyPrec :: Int -> Binds -> Doc

prettyList :: [Binds] -> 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 Exp

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Exp -> Doc

prettyPrec :: Int -> Exp -> Doc

prettyList :: [Exp] -> Doc

Pretty ImportDecl

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportDecl -> Doc

prettyPrec :: Int -> ImportDecl -> Doc

prettyList :: [ImportDecl] -> Doc

Pretty ImportSpec

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ImportSpec -> Doc

prettyPrec :: Int -> ImportSpec -> Doc

prettyList :: [ImportSpec] -> Doc

Pretty Literal

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

Pretty Match

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Match -> Doc

prettyPrec :: Int -> Match -> Doc

prettyList :: [Match] -> Doc

Pretty Module

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Module -> Doc

prettyPrec :: Int -> Module -> Doc

prettyList :: [Module] -> Doc

Pretty ModuleName

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModuleName -> Doc

prettyPrec :: Int -> ModuleName -> Doc

prettyList :: [ModuleName] -> Doc

Pretty ModulePragma

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: ModulePragma -> Doc

prettyPrec :: Int -> ModulePragma -> Doc

prettyList :: [ModulePragma] -> Doc

Pretty Name

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Name -> Doc

prettyPrec :: Int -> Name -> Doc

prettyList :: [Name] -> Doc

Pretty Pat

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Pat -> Doc

prettyPrec :: Int -> Pat -> Doc

prettyList :: [Pat] -> Doc

Pretty QName

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QName -> Doc

prettyPrec :: Int -> QName -> Doc

prettyList :: [QName] -> Doc

Pretty QOp

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: QOp -> Doc

prettyPrec :: Int -> QOp -> Doc

prettyList :: [QOp] -> Doc

Pretty Stmt

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Stmt -> Doc

prettyPrec :: Int -> Stmt -> Doc

prettyList :: [Stmt] -> Doc

Pretty Strictness

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Strictness -> Doc

prettyPrec :: Int -> Strictness -> Doc

prettyList :: [Strictness] -> Doc

Pretty TyVarBind

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: TyVarBind -> Doc

prettyPrec :: Int -> TyVarBind -> Doc

prettyList :: [TyVarBind] -> Doc

Pretty Type

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Type -> Doc

prettyPrec :: Int -> Type -> Doc

prettyList :: [Type] -> 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 Constraint

Defined in Agda.Utils.Warshall

Methods

pretty :: Constraint -> Doc

prettyPrec :: Int -> Constraint -> Doc

prettyList :: [Constraint] -> Doc

Pretty Node

Defined in Agda.Utils.Warshall

Methods

pretty :: Node -> Doc

prettyPrec :: Int -> Node -> Doc

prettyList :: [Node] -> Doc

Pretty SizeExpr

Defined in Agda.Utils.Warshall

Methods

pretty :: SizeExpr -> Doc

prettyPrec :: Int -> SizeExpr -> Doc

prettyList :: [SizeExpr] -> Doc

Pretty Weight

Defined in Agda.Utils.Warshall

Methods

pretty :: Weight -> Doc

prettyPrec :: Int -> Weight -> Doc

prettyList :: [Weight] -> Doc

Pretty Int32

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Int32 -> Doc

prettyPrec :: Int -> Int32 -> Doc

prettyList :: [Int32] -> Doc

Pretty CallStack

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: CallStack -> Doc

prettyPrec :: Int -> CallStack -> Doc

prettyList :: [CallStack] -> Doc

Pretty SrcLoc

Defined in Agda.Utils.CallStack.Pretty

Methods

pretty :: SrcLoc -> Doc

prettyPrec :: Int -> SrcLoc -> Doc

prettyList :: [SrcLoc] -> Doc

Pretty Word64

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Word64 -> Doc

prettyPrec :: Int -> Word64 -> Doc

prettyList :: [Word64] -> Doc

Pretty IntSet

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntSet -> Doc

prettyPrec :: Int -> IntSet -> Doc

prettyList :: [IntSet] -> Doc

Pretty Text

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Text -> Doc

prettyPrec :: Int -> Text -> Doc

prettyList :: [Text] -> Doc

Pretty Integer

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Integer -> Doc

prettyPrec :: Int -> Integer -> Doc

prettyList :: [Integer] -> Doc

Pretty ()

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: () -> Doc

prettyPrec :: Int -> () -> Doc

prettyList :: [()] -> Doc

Pretty Bool

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Bool -> Doc

prettyPrec :: Int -> Bool -> Doc

prettyList :: [Bool] -> Doc

Pretty Char

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Char -> Doc

prettyPrec :: Int -> Char -> Doc

prettyList :: [Char] -> Doc

Pretty Double

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Double -> Doc

prettyPrec :: Int -> Double -> Doc

prettyList :: [Double] -> Doc

Pretty Int

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Int -> Doc

prettyPrec :: Int -> Int -> Doc

prettyList :: [Int] -> 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

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

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: MaybePlaceholder a -> Doc

prettyPrec :: Int -> MaybePlaceholder a -> Doc

prettyList :: [MaybePlaceholder 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 (Ranged a)

Ignores range.

Defined in Agda.Syntax.Common

Methods

pretty :: Ranged a -> Doc

prettyPrec :: Int -> Ranged a -> Doc

prettyList :: [Ranged 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 (WithOrigin a)

Defined in Agda.Syntax.Common

Methods

pretty :: WithOrigin a -> Doc

prettyPrec :: Int -> WithOrigin a -> Doc

prettyList :: [WithOrigin a] -> 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 (TacticAttribute' a)

Defined in Agda.Syntax.Concrete.Pretty

Methods

pretty :: TacticAttribute' a -> Doc

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

prettyList :: [TacticAttribute' 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 t => Pretty (Abs t)

Defined in Agda.Syntax.Internal

Methods

pretty :: Abs t -> Doc

prettyPrec :: Int -> Abs t -> Doc

prettyList :: [Abs t] -> Doc

Pretty a => Pretty (Blocked a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc

prettyPrec :: Int -> Blocked a -> Doc

prettyList :: [Blocked 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 (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' 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 t => Pretty (NotBlocked' t)

Defined in Agda.Syntax.Internal.Blockers

Methods

pretty :: NotBlocked' t -> Doc

prettyPrec :: Int -> NotBlocked' t -> Doc

prettyList :: [NotBlocked' t] -> Doc

Pretty tm => Pretty (Elim' tm)

Defined in Agda.Syntax.Internal.Elim

Methods

pretty :: Elim' tm -> Doc

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

prettyList :: [Elim' tm] -> Doc

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

Defined in Agda.Syntax.Common.Pretty

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

Methods

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

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

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

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

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: PrintRange a -> Doc

prettyPrec :: Int -> PrintRange a -> Doc

prettyList :: [PrintRange a] -> Doc

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

Defined in Agda.Syntax.Common.Pretty

Methods

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

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

prettyList :: [Range' (Maybe a)] -> 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 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 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 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 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 c => Pretty (FunctionInverse' c)

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: FunctionInverse' c -> Doc

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

prettyList :: [FunctionInverse' c] -> Doc

Pretty c => Pretty (IPFace' c)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: IPFace' c -> Doc

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

prettyList :: [IPFace' c] -> Doc

Pretty a => Pretty (Judgement a)

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Judgement a -> Doc

prettyPrec :: Int -> Judgement a -> Doc

prettyList :: [Judgement a] -> Doc

Pretty a => Pretty (Open a)

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Open a -> Doc

prettyPrec :: Int -> Open a -> Doc

prettyList :: [Open 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

(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 n => Pretty (WithUniqueInt n)

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

pretty :: WithUniqueInt n -> Doc

prettyPrec :: Int -> WithUniqueInt n -> Doc

prettyList :: [WithUniqueInt n] -> Doc

Pretty a => Pretty (List1 a)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: List1 a -> Doc

prettyPrec :: Int -> List1 a -> Doc

prettyList :: [List1 a] -> Doc

Pretty a => Pretty (IntMap a)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: IntMap a -> Doc

prettyPrec :: Int -> IntMap a -> Doc

prettyList :: [IntMap a] -> Doc

Pretty a => Pretty (Set a)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Set a -> Doc

prettyPrec :: Int -> Set a -> Doc

prettyList :: [Set a] -> Doc

a ~ Aspects => Pretty (Doc a)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Doc a -> Doc0

prettyPrec :: Int -> Doc a -> Doc0

prettyList :: [Doc a] -> Doc0

Pretty a => Pretty (Maybe a)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Maybe a -> Doc

prettyPrec :: Int -> Maybe a -> Doc

prettyList :: [Maybe a] -> Doc

Pretty a => Pretty [a]

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: [a] -> Doc

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

prettyList :: [[a]] -> 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 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 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 (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 (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 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

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

(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 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 k, Pretty v) => Pretty (Map k v)

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: Map k v -> Doc

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

prettyList :: [Map k v] -> 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 a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c)

Defined in Agda.Utils.Warshall

Methods

pretty :: LegendMatrix a b c -> Doc

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

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

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

Defined in Agda.Syntax.Common

Methods

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

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

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

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

a ? b = hang a 2 b

comma :: Doc

colon :: Doc

parens

Arguments

:: Doc

-> Doc

Wrap document in (...)

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.

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

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

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

vsep :: [Doc] -> Doc

space :: Doc

braces

Arguments

:: Doc

-> Doc

Wrap document in {...}

brackets

Arguments

:: Doc

-> Doc

Wrap document in [...]

semi :: Doc

equals :: Doc

lparen :: Doc

rparen :: Doc

lbrack :: Doc

rbrack :: Doc

lbrace :: Doc

rbrace :: Doc

quotes

Arguments

:: Doc

-> Doc

Wrap document in '...'

doubleQuotes

Arguments

:: Doc

-> Doc

Wrap document in "..."

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

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

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

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

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

Comma separated list, without the brackets.

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

pshow :: Show a => a -> Doc

pshow = text . show

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

Pretty print a set.

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

Pretty print an association list.

pwords :: String -> [Doc]

fwords :: String -> Doc

hsepWith :: Doc -> Doc -> Doc -> Doc

Separate, but only if both separees are not null.

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

Pretty print a single association.

hlSymbol :: Doc -> Doc

mparens :: Bool -> Doc -> Doc

Apply parens to Doc if boolean is true.

parensNonEmpty :: Doc -> Doc

Only wrap in parens if not empty

multiLineText :: String -> Doc

Handles strings with newlines properly (preserving indentation)

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

Used for with-like telescopes

annotateAspect :: Aspect -> Doc -> Doc

Attach a simple Aspect, rather than a full set of Aspects, to a document.

hlComment :: Doc -> Doc

hlKeyword :: Doc -> Doc

hlString :: Doc -> Doc

hlNumber :: Doc -> Doc

hlHole :: Doc -> Doc

hlPrimitiveType :: Doc -> Doc

hlPragma :: Doc -> Doc

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

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

Show Mode

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

Eq Mode

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

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

data Span a

A Span represents the result of an annotation after a Doc has been rendered, capturing where the annotation now starts and ends in the rendered output.

Constructors

Span

Fields

• spanStart :: !Int
• spanLength :: !Int
• spanAnnotation :: a

Instances

Functor Span

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

fmap :: (a -> b) -> Span a -> Span b

(<$) :: a -> Span b -> Span a

Show a => Show (Span a)

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Span a -> ShowS

show :: Span a -> String

showList :: [Span a] -> ShowS

Eq a => Eq (Span a)

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

(==) :: Span a -> Span a -> Bool

(/=) :: Span a -> Span a -> Bool

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

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

Show Style

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

showsPrec :: Int -> Style -> ShowS

show :: Style -> String

showList :: [Style] -> ShowS

Eq Style

Defined in Text.PrettyPrint.Annotated.HughesPJ

Methods

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

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

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

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

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.

int

Arguments

:: Int

-> Doc a

int n = text (show n)

integer

Arguments

:: Integer

-> Doc a

integer n = text (show n)

float

Arguments

:: Float

-> Doc a

float n = text (show n)

double

Arguments

:: Double

-> Doc a

double n = text (show n)

char :: Char -> Doc a

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

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

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

isEmpty :: Doc a -> Bool

Returns True if the document is empty

style :: Style

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

render :: Doc a -> String

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

annotate :: a -> Doc a -> Doc a

Attach an annotation to a document.

ptext :: String -> Doc a

Same as text. Used to be used for Bytestrings.

sizedText :: Int -> String -> Doc a

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

zeroWidthText :: String -> Doc a

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

rational

Arguments

:: Rational

-> Doc a

rational n = text (show n)

nest :: Int -> Doc a -> Doc a

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

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

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

($$) :: Doc a -> Doc a -> Doc a 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 a -> Doc a -> Doc a infixl 5

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

cat :: [Doc a] -> Doc a

Either hcat or vcat.

fcat :: [Doc a] -> Doc a

"Paragraph fill" version of cat.

renderStyle :: Style -> Doc a -> 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 b

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.

fullRenderAnn

Arguments

:: Mode

Rendering mode.

-> Int

Line length.

-> Float

Ribbons per line.

-> (AnnotDetails b -> a -> a)

What to do with text.

-> a

What to do at the end.

-> Doc b

The document.

-> a

Result.

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

renderSpans :: Doc ann -> (String, [Span ann])

Render an annotated Doc to a String and list of annotations (see Span) using the default Style (see style).

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

An associative operation.

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