Render.Class

Documentation

class Render a where

Typeclass for rendering Inlines

Minimal complete definition

Nothing

Methods

render :: a -> Inlines

renderPrec :: Int -> a -> Inlines

Instances

Render Name

Abstract

Defined in Render.Name

Methods

render :: Name -> Inlines

renderPrec :: Int -> Name -> Inlines

Render QName

Defined in Render.Name

Methods

render :: QName -> Inlines

renderPrec :: Int -> QName -> Inlines

Render Cohesion

Defined in Render.Common

Methods

render :: Cohesion -> Inlines

renderPrec :: Int -> Cohesion -> Inlines

Render Fixity

Defined in Render.Concrete

Methods

render :: Fixity -> Inlines

renderPrec :: Int -> Fixity -> Inlines

Render Fixity'

Defined in Render.Concrete

Methods

render :: Fixity' -> Inlines

renderPrec :: Int -> Fixity' -> Inlines

Render GenPart

Defined in Render.Concrete

Methods

render :: GenPart -> Inlines

renderPrec :: Int -> GenPart -> Inlines

Render Induction

Defined in Render.Common

Methods

render :: Induction -> Inlines

renderPrec :: Int -> Induction -> Inlines

Render InteractionId

InteractionId

Defined in Render.Concrete

Methods

render :: InteractionId -> Inlines

renderPrec :: Int -> InteractionId -> Inlines

Render MetaId

MetaId

Defined in Render.Common

Methods

render :: MetaId -> Inlines

renderPrec :: Int -> MetaId -> Inlines

Render Modality

Defined in Render.Concrete

Methods

render :: Modality -> Inlines

renderPrec :: Int -> Modality -> Inlines

Render NameId

NameId

Defined in Render.Common

Methods

render :: NameId -> Inlines

renderPrec :: Int -> NameId -> Inlines

Render ProblemId

Defined in Render.TypeChecking

Methods

render :: ProblemId -> Inlines

renderPrec :: Int -> ProblemId -> Inlines

Render Quantity

Quantity

Defined in Render.Common

Methods

render :: Quantity -> Inlines

renderPrec :: Int -> Quantity -> Inlines

Render QωOrigin

Defined in Render.Common

Methods

render :: QωOrigin -> Inlines

renderPrec :: Int -> QωOrigin -> Inlines

Render Relevance

Relevance

Defined in Render.Common

Methods

render :: Relevance -> Inlines

renderPrec :: Int -> Relevance -> Inlines

Render BoundName

Defined in Render.Concrete

Methods

render :: BoundName -> Inlines

renderPrec :: Int -> BoundName -> Inlines

Render Declaration

Defined in Render.Concrete

Methods

render :: Declaration -> Inlines

renderPrec :: Int -> Declaration -> Inlines

Render DoStmt

Defined in Render.Concrete

Methods

render :: DoStmt -> Inlines

renderPrec :: Int -> DoStmt -> Inlines

Render Expr

Expression

Defined in Render.Concrete

Methods

render :: Expr -> Inlines

renderPrec :: Int -> Expr -> Inlines

Render LHS

Defined in Render.Concrete

Methods

render :: LHS -> Inlines

renderPrec :: Int -> LHS -> Inlines

Render LHSCore

Defined in Render.Concrete

Methods

render :: LHSCore -> Inlines

renderPrec :: Int -> LHSCore -> Inlines

Render LamBinding

LamBinding

Defined in Render.Concrete

Methods

render :: LamBinding -> Inlines

renderPrec :: Int -> LamBinding -> Inlines

Render LamClause

Defined in Render.Concrete

Methods

render :: LamClause -> Inlines

renderPrec :: Int -> LamClause -> Inlines

Render ModuleApplication

Defined in Render.Concrete

Methods

render :: ModuleApplication -> Inlines

renderPrec :: Int -> ModuleApplication -> Inlines

Render ModuleAssignment

Defined in Render.Concrete

Methods

render :: ModuleAssignment -> Inlines

renderPrec :: Int -> ModuleAssignment -> Inlines

Render OpenShortHand

Defined in Render.Concrete

Methods

render :: OpenShortHand -> Inlines

renderPrec :: Int -> OpenShortHand -> Inlines

Render Pattern

Defined in Render.Concrete

Methods

render :: Pattern -> Inlines

renderPrec :: Int -> Pattern -> Inlines

Render Pragma

Defined in Render.Concrete

Methods

render :: Pragma -> Inlines

renderPrec :: Int -> Pragma -> Inlines

Render RHS

Defined in Render.Concrete

Methods

render :: RHS -> Inlines

renderPrec :: Int -> RHS -> Inlines

Render TypedBinding

TypedBinding

Defined in Render.Concrete

Methods

render :: TypedBinding -> Inlines

renderPrec :: Int -> TypedBinding -> Inlines

Render WhereClause

Defined in Render.Concrete

Methods

render :: WhereClause -> Inlines

renderPrec :: Int -> WhereClause -> Inlines

Render Name

Defined in Render.Name

Methods

render :: Name -> Inlines

renderPrec :: Int -> Name -> Inlines

Render NamePart

Concrete

Defined in Render.Name

Methods

render :: NamePart -> Inlines

renderPrec :: Int -> NamePart -> Inlines

Render QName

Defined in Render.Name

Methods

render :: QName -> Inlines

renderPrec :: Int -> QName -> Inlines

Render NamedBinding

NamedBinding

Defined in Render.Concrete

Methods

render :: NamedBinding -> Inlines

renderPrec :: Int -> NamedBinding -> Inlines

Render Tel

Defined in Render.Concrete

Methods

render :: Tel -> Inlines

renderPrec :: Int -> Tel -> Inlines

Render Clause

Defined in Render.Internal

Methods

render :: Clause -> Inlines

renderPrec :: Int -> Clause -> Inlines

Render DBPatVar

Defined in Render.Internal

Methods

render :: DBPatVar -> Inlines

renderPrec :: Int -> DBPatVar -> Inlines

Render Level

Defined in Render.Internal

Methods

render :: Level -> Inlines

renderPrec :: Int -> Level -> Inlines

Render PlusLevel

Defined in Render.Internal

Methods

render :: PlusLevel -> Inlines

renderPrec :: Int -> PlusLevel -> Inlines

Render Sort

Defined in Render.Internal

Methods

render :: Sort -> Inlines

renderPrec :: Int -> Sort -> Inlines

Render Term

Term

Defined in Render.Internal

Methods

render :: Term -> Inlines

renderPrec :: Int -> Term -> Inlines

Render Type

Defined in Render.Internal

Methods

render :: Type -> Inlines

renderPrec :: Int -> Type -> Inlines

Render Blocker

Defined in Render.Internal

Methods

render :: Blocker -> Inlines

renderPrec :: Int -> Blocker -> Inlines

Render Literal

Literal

Defined in Render.Literal

Methods

render :: Literal -> Inlines

renderPrec :: Int -> Literal -> Inlines

Render IntervalWithoutFile

Defined in Render.Position

Methods

render :: IntervalWithoutFile -> Inlines

renderPrec :: Int -> IntervalWithoutFile -> Inlines

Render PositionWithoutFile

Defined in Render.Position

Methods

render :: PositionWithoutFile -> Inlines

renderPrec :: Int -> PositionWithoutFile -> Inlines

Render Comparison

Defined in Render.TypeChecking

Methods

render :: Comparison -> Inlines

renderPrec :: Int -> Comparison -> Inlines

Render NamedMeta

Defined in Render.TypeChecking

Methods

render :: NamedMeta -> Inlines

renderPrec :: Int -> NamedMeta -> Inlines

Render Polarity

Defined in Render.TypeChecking

Methods

render :: Polarity -> Inlines

renderPrec :: Int -> Polarity -> Inlines

Render Occurrence

Defined in Render.TypeChecking

Methods

render :: Occurrence -> Inlines

renderPrec :: Int -> Occurrence -> Inlines

Render AbsolutePath

Defined in Render.Position

Methods

render :: AbsolutePath -> Inlines

renderPrec :: Int -> AbsolutePath -> Inlines

Render CPUTime

Defined in Render.Utils

Methods

render :: CPUTime -> Inlines

renderPrec :: Int -> CPUTime -> Inlines

Render Int32

Defined in Render.Class

Methods

render :: Int32 -> Inlines

renderPrec :: Int -> Int32 -> Inlines

Render Doc

Defined in Render.Class

Methods

render :: Doc -> Inlines

renderPrec :: Int -> Doc -> Inlines

Render Integer

Defined in Render.Class

Methods

render :: Integer -> Inlines

renderPrec :: Int -> Integer -> Inlines

Render Bool

Defined in Render.Class

Methods

render :: Bool -> Inlines

renderPrec :: Int -> Bool -> Inlines

Render Int

Other instances of Render

Defined in Render.Class

Methods

render :: Int -> Inlines

renderPrec :: Int -> Int -> Inlines

Render a => Render (Arg a)

Arg

Defined in Render.Concrete

Methods

render :: Arg a -> Inlines

renderPrec :: Int -> Arg a -> Inlines

Render a => Render (MaybePlaceholder a)

MaybePlaceholder

Defined in Render.Concrete

Methods

render :: MaybePlaceholder a -> Inlines

renderPrec :: Int -> MaybePlaceholder a -> Inlines

Render a => Render (WithHiding a)

Defined in Render.Concrete

Methods

render :: WithHiding a -> Inlines

renderPrec :: Int -> WithHiding a -> Inlines

Render a => Render (Binder' a)

Defined in Render.Concrete

Methods

render :: Binder' a -> Inlines

renderPrec :: Int -> Binder' a -> Inlines

Render a => Render (FieldAssignment' a)

Defined in Render.Concrete

Methods

render :: FieldAssignment' a -> Inlines

renderPrec :: Int -> FieldAssignment' a -> Inlines

Render (OpApp Expr)

OpApp

Defined in Render.Concrete

Methods

render :: OpApp Expr -> Inlines

renderPrec :: Int -> OpApp Expr -> Inlines

Render a => Render (Pattern' a)

Defined in Render.Internal

Methods

render :: Pattern' a -> Inlines

renderPrec :: Int -> Pattern' a -> Inlines

Render a => Render (Substitution' a)

Defined in Render.Internal

Methods

render :: Substitution' a -> Inlines

renderPrec :: Int -> Substitution' a -> Inlines

Render a => Render (Tele (Dom a))

Defined in Render.Internal

Methods

render :: Tele (Dom a) -> Inlines

renderPrec :: Int -> Tele (Dom a) -> Inlines

Render tm => Render (Elim' tm)

Defined in Render.Internal

Methods

render :: Elim' tm -> Inlines

renderPrec :: Int -> Elim' tm -> Inlines

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

Defined in Render.Position

Methods

render :: Interval' (Maybe a) -> Inlines

renderPrec :: Int -> Interval' (Maybe a) -> Inlines

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

Defined in Render.Position

Methods

render :: Position' (Maybe a) -> Inlines

renderPrec :: Int -> Position' (Maybe a) -> Inlines

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

Defined in Render.Position

Methods

render :: Range' (Maybe a) -> Inlines

renderPrec :: Int -> Range' (Maybe a) -> Inlines

Render c => Render (IPBoundary' c)

IPBoundary'

Defined in Render.Interaction

Methods

render :: IPBoundary' c -> Inlines

renderPrec :: Int -> IPBoundary' c -> Inlines

Render a => Render (List1 a)

Defined in Render.Class

Methods

render :: List1 a -> Inlines

renderPrec :: Int -> List1 a -> Inlines

Render a => Render (List2 a)

Defined in Render.Class

Methods

render :: List2 a -> Inlines

renderPrec :: Int -> List2 a -> Inlines

Render a => Render [a]

Defined in Render.Class

Methods

render :: [a] -> Inlines

renderPrec :: Int -> [a] -> Inlines

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

OutputConstraint

Defined in Render.Interaction

Methods

render :: OutputConstraint a b -> Inlines

renderPrec :: Int -> OutputConstraint a b -> Inlines

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

OutputForm

Defined in Render.Interaction

Methods

render :: OutputForm a b -> Inlines

renderPrec :: Int -> OutputForm a b -> Inlines

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

Defined in Render.Concrete

Methods

render :: ImportDirective' a b -> Inlines

renderPrec :: Int -> ImportDirective' a b -> Inlines

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

Defined in Render.Concrete

Methods

render :: ImportedName' a b -> Inlines

renderPrec :: Int -> ImportedName' a b -> Inlines

Render e => Render (Named NamedName e)

Named NamedName (Named_)

Defined in Render.Concrete

Methods

render :: Named NamedName e -> Inlines

renderPrec :: Int -> Named NamedName e -> Inlines

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

Defined in Render.Concrete

Methods

render :: Renaming' a b -> Inlines

renderPrec :: Int -> Renaming' a b -> Inlines

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

Defined in Render.Concrete

Methods

render :: Using' a b -> Inlines

renderPrec :: Int -> Using' a b -> Inlines

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

Defined in Render.Internal

Methods

render :: Dom' t e -> Inlines

renderPrec :: Int -> Dom' t e -> Inlines

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

Defined in Render.Concrete

Methods

render :: Either a b -> Inlines

renderPrec :: Int -> Either a b -> Inlines

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

Defined in Render.Common

Methods

render :: RewriteEqn' qn nm p e -> Inlines

renderPrec :: Int -> RewriteEqn' qn nm p e -> Inlines

renderM :: (Applicative m, Render a) => a -> m Inlines

Rendering undersome context class RenderTCM a where renderTCM :: a -> Agda.TCM Inlines

Simply "pure . render"

renderP :: (Applicative m, Pretty a) => a -> m Inlines

Render instances of Pretty

renderA :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines

like prettyA

renderATop :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines

like prettyATop