Safe Haskell	None
Language	Haskell2010

Render.Class

Synopsis

class Render a where
- render :: a -> Inlines
- renderPrec :: Int -> a -> Inlines
renderM :: (Applicative m, Render a) => a -> m Inlines
renderP :: (Applicative m, Pretty a) => a -> m Inlines
renderA :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines
renderATop :: (Render c, ToConcrete a, ConOfAbs a ~ c) => a -> TCM Inlines

Documentation

class Render a where Source #

Typeclass for rendering Inlines

Minimal complete definition

Nothing

Methods

render :: a -> Inlines Source #

renderPrec :: Int -> a -> Inlines Source #

Instances

Instances details

Render Bool Source #
Instance details Defined in Render.Class Methods render :: Bool -> Inlines Source # renderPrec :: Int -> Bool -> Inlines Source #
Render Int Source #	Other instances of Render
Instance details Defined in Render.Class Methods render :: Int -> Inlines Source # renderPrec :: Int -> Int -> Inlines Source #
Render Int32 Source #
Instance details Defined in Render.Class Methods render :: Int32 -> Inlines Source # renderPrec :: Int -> Int32 -> Inlines Source #
Render Integer Source #
Instance details Defined in Render.Class Methods render :: Integer -> Inlines Source # renderPrec :: Int -> Integer -> Inlines Source #
Render Term Source #	Term
Instance details Defined in Render.Internal Methods render :: Term -> Inlines Source # renderPrec :: Int -> Term -> Inlines Source #
Render Type Source #
Instance details Defined in Render.Internal Methods render :: Type -> Inlines Source # renderPrec :: Int -> Type -> Inlines Source #
Render Sort Source #
Instance details Defined in Render.Internal Methods render :: Sort -> Inlines Source # renderPrec :: Int -> Sort -> Inlines Source #
Render Level Source #
Instance details Defined in Render.Internal Methods render :: Level -> Inlines Source # renderPrec :: Int -> Level -> Inlines Source #
Render PlusLevel Source #
Instance details Defined in Render.Internal Methods render :: PlusLevel -> Inlines Source # renderPrec :: Int -> PlusLevel -> Inlines Source #
Render Clause Source #
Instance details Defined in Render.Internal Methods render :: Clause -> Inlines Source # renderPrec :: Int -> Clause -> Inlines Source #
Render DBPatVar Source #
Instance details Defined in Render.Internal Methods render :: DBPatVar -> Inlines Source # renderPrec :: Int -> DBPatVar -> Inlines Source #
Render Blocker Source #
Instance details Defined in Render.Internal Methods render :: Blocker -> Inlines Source # renderPrec :: Int -> Blocker -> Inlines Source #
Render NamedBinding Source #	NamedBinding
Instance details Defined in Render.Concrete Methods render :: NamedBinding -> Inlines Source # renderPrec :: Int -> NamedBinding -> Inlines Source #
Render Tel Source #
Instance details Defined in Render.Concrete Methods render :: Tel -> Inlines Source # renderPrec :: Int -> Tel -> Inlines Source #
Render ModuleAssignment Source #
Instance details Defined in Render.Concrete Methods render :: ModuleAssignment -> Inlines Source # renderPrec :: Int -> ModuleAssignment -> Inlines Source #
Render Expr Source #	Expression
Instance details Defined in Render.Concrete Methods render :: Expr -> Inlines Source # renderPrec :: Int -> Expr -> Inlines Source #
Render Pattern Source #
Instance details Defined in Render.Concrete Methods render :: Pattern -> Inlines Source # renderPrec :: Int -> Pattern -> Inlines Source #
Render DoStmt Source #
Instance details Defined in Render.Concrete Methods render :: DoStmt -> Inlines Source # renderPrec :: Int -> DoStmt -> Inlines Source #
Render LamBinding Source #	LamBinding
Instance details Defined in Render.Concrete Methods render :: LamBinding -> Inlines Source # renderPrec :: Int -> LamBinding -> Inlines Source #
Render BoundName Source #
Instance details Defined in Render.Concrete Methods render :: BoundName -> Inlines Source # renderPrec :: Int -> BoundName -> Inlines Source #
Render TypedBinding Source #	TypedBinding
Instance details Defined in Render.Concrete Methods render :: TypedBinding -> Inlines Source # renderPrec :: Int -> TypedBinding -> Inlines Source #
Render LHS Source #
Instance details Defined in Render.Concrete Methods render :: LHS -> Inlines Source # renderPrec :: Int -> LHS -> Inlines Source #
Render LHSCore Source #
Instance details Defined in Render.Concrete Methods render :: LHSCore -> Inlines Source # renderPrec :: Int -> LHSCore -> Inlines Source #
Render RHS Source #
Instance details Defined in Render.Concrete Methods render :: RHS -> Inlines Source # renderPrec :: Int -> RHS -> Inlines Source #
Render WhereClause Source #
Instance details Defined in Render.Concrete Methods render :: WhereClause -> Inlines Source # renderPrec :: Int -> WhereClause -> Inlines Source #
Render LamClause Source #
Instance details Defined in Render.Concrete Methods render :: LamClause -> Inlines Source # renderPrec :: Int -> LamClause -> Inlines Source #
Render Declaration Source #
Instance details Defined in Render.Concrete Methods render :: Declaration -> Inlines Source # renderPrec :: Int -> Declaration -> Inlines Source #
Render ModuleApplication Source #
Instance details Defined in Render.Concrete Methods render :: ModuleApplication -> Inlines Source # renderPrec :: Int -> ModuleApplication -> Inlines Source #
Render OpenShortHand Source #
Instance details Defined in Render.Concrete Methods render :: OpenShortHand -> Inlines Source # renderPrec :: Int -> OpenShortHand -> Inlines Source #
Render Pragma Source #
Instance details Defined in Render.Concrete Methods render :: Pragma -> Inlines Source # renderPrec :: Int -> Pragma -> Inlines Source #
Render Occurrence Source #
Instance details Defined in Render.TypeChecking Methods render :: Occurrence -> Inlines Source # renderPrec :: Int -> Occurrence -> Inlines Source #
Render Literal Source #	Literal
Instance details Defined in Render.Literal Methods render :: Literal -> Inlines Source # renderPrec :: Int -> Literal -> Inlines Source #
Render Name Source #	Abstract
Instance details Defined in Render.Name Methods render :: Name -> Inlines Source # renderPrec :: Int -> Name -> Inlines Source #
Render QName Source #
Instance details Defined in Render.Name Methods render :: QName -> Inlines Source # renderPrec :: Int -> QName -> Inlines Source #
Render NamedMeta Source #
Instance details Defined in Render.TypeChecking Methods render :: NamedMeta -> Inlines Source # renderPrec :: Int -> NamedMeta -> Inlines Source #
Render Comparison Source #
Instance details Defined in Render.TypeChecking Methods render :: Comparison -> Inlines Source # renderPrec :: Int -> Comparison -> Inlines Source #
Render Polarity Source #
Instance details Defined in Render.TypeChecking Methods render :: Polarity -> Inlines Source # renderPrec :: Int -> Polarity -> Inlines Source #
Render Name Source #
Instance details Defined in Render.Name Methods render :: Name -> Inlines Source # renderPrec :: Int -> Name -> Inlines Source #
Render NamePart Source #	Concrete
Instance details Defined in Render.Name Methods render :: NamePart -> Inlines Source # renderPrec :: Int -> NamePart -> Inlines Source #
Render QName Source #
Instance details Defined in Render.Name Methods render :: QName -> Inlines Source # renderPrec :: Int -> QName -> Inlines Source #
Render Induction Source #
Instance details Defined in Render.Common Methods render :: Induction -> Inlines Source # renderPrec :: Int -> Induction -> Inlines Source #
Render Modality Source #
Instance details Defined in Render.Concrete Methods render :: Modality -> Inlines Source # renderPrec :: Int -> Modality -> Inlines Source #
Render QωOrigin Source #
Instance details Defined in Render.Common Methods render :: QωOrigin -> Inlines Source # renderPrec :: Int -> QωOrigin -> Inlines Source #
Render Quantity Source #	Quantity
Instance details Defined in Render.Common Methods render :: Quantity -> Inlines Source # renderPrec :: Int -> Quantity -> Inlines Source #
Render Relevance Source #	Relevance
Instance details Defined in Render.Common Methods render :: Relevance -> Inlines Source # renderPrec :: Int -> Relevance -> Inlines Source #
Render Cohesion Source #
Instance details Defined in Render.Common Methods render :: Cohesion -> Inlines Source # renderPrec :: Int -> Cohesion -> Inlines Source #
Render NameId Source #	NameId
Instance details Defined in Render.Common Methods render :: NameId -> Inlines Source # renderPrec :: Int -> NameId -> Inlines Source #
Render MetaId Source #	MetaId
Instance details Defined in Render.Common Methods render :: MetaId -> Inlines Source # renderPrec :: Int -> MetaId -> Inlines Source #
Render ProblemId Source #
Instance details Defined in Render.TypeChecking Methods render :: ProblemId -> Inlines Source # renderPrec :: Int -> ProblemId -> Inlines Source #
Render InteractionId Source #	InteractionId
Instance details Defined in Render.Concrete Methods render :: InteractionId -> Inlines Source # renderPrec :: Int -> InteractionId -> Inlines Source #
Render Fixity Source #
Instance details Defined in Render.Concrete Methods render :: Fixity -> Inlines Source # renderPrec :: Int -> Fixity -> Inlines Source #
Render Fixity' Source #
Instance details Defined in Render.Concrete Methods render :: Fixity' -> Inlines Source # renderPrec :: Int -> Fixity' -> Inlines Source #
Render GenPart Source #
Instance details Defined in Render.Concrete Methods render :: GenPart -> Inlines Source # renderPrec :: Int -> GenPart -> Inlines Source #
Render PositionWithoutFile Source #
Instance details Defined in Render.Position Methods render :: PositionWithoutFile -> Inlines Source # renderPrec :: Int -> PositionWithoutFile -> Inlines Source #
Render IntervalWithoutFile Source #
Instance details Defined in Render.Position Methods render :: IntervalWithoutFile -> Inlines Source # renderPrec :: Int -> IntervalWithoutFile -> Inlines Source #
Render AbsolutePath Source #
Instance details Defined in Render.Position Methods render :: AbsolutePath -> Inlines Source # renderPrec :: Int -> AbsolutePath -> Inlines Source #
Render CPUTime Source #
Instance details Defined in Render.Utils Methods render :: CPUTime -> Inlines Source # renderPrec :: Int -> CPUTime -> Inlines Source #
Render Doc Source #
Instance details Defined in Render.Class Methods render :: Doc -> Inlines Source # renderPrec :: Int -> Doc -> Inlines Source #
Render a => Render [a] Source #
Instance details Defined in Render.Class Methods render :: [a] -> Inlines Source # renderPrec :: Int -> [a] -> Inlines Source #
Render c => Render (IPBoundary' c) Source #	IPBoundary'
Instance details Defined in Render.Interaction Methods render :: IPBoundary' c -> Inlines Source # renderPrec :: Int -> IPBoundary' c -> Inlines Source #
Render a => Render (Tele (Dom a)) Source #
Instance details Defined in Render.Internal Methods render :: Tele (Dom a) -> Inlines Source # renderPrec :: Int -> Tele (Dom a) -> Inlines Source #
Render a => Render (Pattern' a) Source #
Instance details Defined in Render.Internal Methods render :: Pattern' a -> Inlines Source # renderPrec :: Int -> Pattern' a -> Inlines Source #
Render a => Render (Substitution' a) Source #
Instance details Defined in Render.Internal Methods render :: Substitution' a -> Inlines Source # renderPrec :: Int -> Substitution' a -> Inlines Source #
Render tm => Render (Elim' tm) Source #
Instance details Defined in Render.Internal Methods render :: Elim' tm -> Inlines Source # renderPrec :: Int -> Elim' tm -> Inlines Source #
Render (OpApp Expr) Source #	OpApp
Instance details Defined in Render.Concrete Methods render :: OpApp Expr -> Inlines Source # renderPrec :: Int -> OpApp Expr -> Inlines Source #
Render a => Render (FieldAssignment' a) Source #
Instance details Defined in Render.Concrete Methods render :: FieldAssignment' a -> Inlines Source # renderPrec :: Int -> FieldAssignment' a -> Inlines Source #
Render a => Render (Binder' a) Source #
Instance details Defined in Render.Concrete Methods render :: Binder' a -> Inlines Source # renderPrec :: Int -> Binder' a -> Inlines Source #
Render a => Render (WithHiding a) Source #
Instance details Defined in Render.Concrete Methods render :: WithHiding a -> Inlines Source # renderPrec :: Int -> WithHiding a -> Inlines Source #
Render a => Render (Arg a) Source #	Arg
Instance details Defined in Render.Concrete Methods render :: Arg a -> Inlines Source # renderPrec :: Int -> Arg a -> Inlines Source #
Render a => Render (MaybePlaceholder a) Source #	MaybePlaceholder
Instance details Defined in Render.Concrete Methods render :: MaybePlaceholder a -> Inlines Source # renderPrec :: Int -> MaybePlaceholder a -> Inlines Source #
Render a => Render (Position' (Maybe a)) Source #
Instance details Defined in Render.Position Methods render :: Position' (Maybe a) -> Inlines Source # renderPrec :: Int -> Position' (Maybe a) -> Inlines Source #
Render a => Render (Interval' (Maybe a)) Source #
Instance details Defined in Render.Position Methods render :: Interval' (Maybe a) -> Inlines Source # renderPrec :: Int -> Interval' (Maybe a) -> Inlines Source #
Render a => Render (Range' (Maybe a)) Source #
Instance details Defined in Render.Position Methods render :: Range' (Maybe a) -> Inlines Source # renderPrec :: Int -> Range' (Maybe a) -> Inlines Source #
Render a => Render (List2 a) Source #
Instance details Defined in Render.Class Methods render :: List2 a -> Inlines Source # renderPrec :: Int -> List2 a -> Inlines Source #
Render a => Render (List1 a) Source #
Instance details Defined in Render.Class Methods render :: List1 a -> Inlines Source # renderPrec :: Int -> List1 a -> Inlines Source #
(Render a, Render b) => Render (Either a b) Source #
Instance details Defined in Render.Concrete Methods render :: Either a b -> Inlines Source # renderPrec :: Int -> Either a b -> Inlines Source #
(Render a, Render b) => Render (OutputForm a b) Source #	OutputForm
Instance details Defined in Render.Interaction Methods render :: OutputForm a b -> Inlines Source # renderPrec :: Int -> OutputForm a b -> Inlines Source #
(Render a, Render b) => Render (OutputConstraint a b) Source #	OutputConstraint
Instance details Defined in Render.Interaction Methods render :: OutputConstraint a b -> Inlines Source # renderPrec :: Int -> OutputConstraint a b -> Inlines Source #
(Render t, Render e) => Render (Dom' t e) Source #
Instance details Defined in Render.Internal Methods render :: Dom' t e -> Inlines Source # renderPrec :: Int -> Dom' t e -> Inlines Source #
Render e => Render (Named NamedName e) Source #	Named NamedName (Named_)
Instance details Defined in Render.Concrete Methods render :: Named NamedName e -> Inlines Source # renderPrec :: Int -> Named NamedName e -> Inlines Source #
(Render a, Render b) => Render (ImportDirective' a b) Source #
Instance details Defined in Render.Concrete Methods render :: ImportDirective' a b -> Inlines Source # renderPrec :: Int -> ImportDirective' a b -> Inlines Source #
(Render a, Render b) => Render (Using' a b) Source #
Instance details Defined in Render.Concrete Methods render :: Using' a b -> Inlines Source # renderPrec :: Int -> Using' a b -> Inlines Source #
(Render a, Render b) => Render (ImportedName' a b) Source #
Instance details Defined in Render.Concrete Methods render :: ImportedName' a b -> Inlines Source # renderPrec :: Int -> ImportedName' a b -> Inlines Source #
(Render a, Render b) => Render (Renaming' a b) Source #
Instance details Defined in Render.Concrete Methods render :: Renaming' a b -> Inlines Source # renderPrec :: Int -> Renaming' a b -> Inlines Source #
(Render p, Render e) => Render (RewriteEqn' qn nm p e) Source #
Instance details Defined in Render.Common Methods render :: RewriteEqn' qn nm p e -> Inlines Source # renderPrec :: Int -> RewriteEqn' qn nm p e -> Inlines Source #

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

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

Simply "pure . render"

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

Render instances of Pretty

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

like prettyA

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

like prettyATop