Agda.Syntax.Common.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 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 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 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 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 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 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 NamedRigid

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: NamedRigid -> Doc

prettyPrec :: Int -> NamedRigid -> Doc

prettyList :: [NamedRigid] -> Doc

Pretty SizeMeta

Defined in Agda.TypeChecking.SizedTypes.Solve

Methods

pretty :: SizeMeta -> Doc

prettyPrec :: Int -> SizeMeta -> Doc

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

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.

prettyShow :: Pretty a => a -> String

Use instead of show when printing to world.

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

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

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

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

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

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

parens

Arguments

:: Doc

-> Doc

Wrap document in (...)

brackets

Arguments

:: Doc

-> Doc

Wrap document in [...]

braces

Arguments

:: Doc

-> Doc

Wrap document in {...}

quotes

Arguments

:: Doc

-> Doc

Wrap document in '...'

doubleQuotes

Arguments

:: Doc

-> Doc

Wrap document in "..."

semi :: Doc

comma :: Doc

colon :: Doc

space :: Doc

equals :: Doc

lparen :: Doc

rparen :: Doc

lbrack :: Doc

rbrack :: Doc

lbrace :: Doc

rbrace :: Doc

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

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

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

Constructors

PageMode

ZigZagMode

LeftMode

OneLineMode

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 Style

Constructors

Style

Fields

• mode :: Mode
• lineLength :: Int
• ribbonsPerLine :: Float

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

data Span a

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

pattern Chr :: !Char -> TextDetails

pattern PStr :: String -> TextDetails

text :: String -> Doc a

render :: Doc a -> String

char :: Char -> Doc a

integer :: Integer -> Doc a

isEmpty :: Doc a -> Bool

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

cat :: [Doc a] -> Doc a

($$) :: Doc a -> Doc a -> Doc a

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

($+$) :: Doc a -> Doc a -> Doc a

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

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

double :: Double -> Doc a

fcat :: [Doc a] -> Doc a

float :: Float -> Doc a

fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc b -> a

fullRenderAnn :: Mode -> Int -> Float -> (AnnotDetails b -> a -> a) -> a -> Doc b -> a

int :: Int -> Doc a

ptext :: String -> Doc a

rational :: Rational -> Doc a

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

renderStyle :: Style -> Doc a -> String

sizedText :: Int -> String -> Doc a

style :: Style

zeroWidthText :: String -> Doc a

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