agda-language-server-0.2.6.2.2: An implementation of language server protocal (LSP) for Agda 2.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Render.Class

Synopsis

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 Name Source #

Abstract

Instance details

Defined in Render.Name

Render QName Source # 
Instance details

Defined in Render.Name

Render Cohesion Source # 
Instance details

Defined in Render.Common

Render Fixity Source # 
Instance details

Defined in Render.Concrete

Render Fixity' Source # 
Instance details

Defined in Render.Concrete

Render GenPart Source # 
Instance details

Defined in Render.Concrete

Render Induction Source # 
Instance details

Defined in Render.Common

Render InteractionId Source #

InteractionId

Instance details

Defined in Render.Concrete

Render MetaId Source #

MetaId

Instance details

Defined in Render.Common

Render Modality Source # 
Instance details

Defined in Render.Concrete

Render NameId Source #

NameId

Instance details

Defined in Render.Common

Render ProblemId Source # 
Instance details

Defined in Render.TypeChecking

Render Quantity Source #

Quantity

Instance details

Defined in Render.Common

Render QωOrigin Source # 
Instance details

Defined in Render.Common

Render Relevance Source #

Relevance

Instance details

Defined in Render.Common

Render BoundName Source # 
Instance details

Defined in Render.Concrete

Render Declaration Source # 
Instance details

Defined in Render.Concrete

Render DoStmt Source # 
Instance details

Defined in Render.Concrete

Render Expr Source #

Expression

Instance details

Defined in Render.Concrete

Render LHS Source # 
Instance details

Defined in Render.Concrete

Render LHSCore Source # 
Instance details

Defined in Render.Concrete

Render LamBinding Source #

LamBinding

Instance details

Defined in Render.Concrete

Render LamClause Source # 
Instance details

Defined in Render.Concrete

Render ModuleApplication Source # 
Instance details

Defined in Render.Concrete

Render ModuleAssignment Source # 
Instance details

Defined in Render.Concrete

Render OpenShortHand Source # 
Instance details

Defined in Render.Concrete

Render Pattern Source # 
Instance details

Defined in Render.Concrete

Render Pragma Source # 
Instance details

Defined in Render.Concrete

Render RHS Source # 
Instance details

Defined in Render.Concrete

Render TypedBinding Source #

TypedBinding

Instance details

Defined in Render.Concrete

Render WhereClause Source # 
Instance details

Defined in Render.Concrete

Render Name Source # 
Instance details

Defined in Render.Name

Render NamePart Source #

Concrete

Instance details

Defined in Render.Name

Render QName Source # 
Instance details

Defined in Render.Name

Render NamedBinding Source #

NamedBinding

Instance details

Defined in Render.Concrete

Render Tel Source # 
Instance details

Defined in Render.Concrete

Render Clause Source # 
Instance details

Defined in Render.Internal

Render DBPatVar Source # 
Instance details

Defined in Render.Internal

Render Level Source # 
Instance details

Defined in Render.Internal

Render PlusLevel Source # 
Instance details

Defined in Render.Internal

Render Sort Source # 
Instance details

Defined in Render.Internal

Render Term Source #

Term

Instance details

Defined in Render.Internal

Render Type Source # 
Instance details

Defined in Render.Internal

Render Blocker Source # 
Instance details

Defined in Render.Internal

Render Literal Source #

Literal

Instance details

Defined in Render.Literal

Render IntervalWithoutFile Source # 
Instance details

Defined in Render.Position

Render PositionWithoutFile Source # 
Instance details

Defined in Render.Position

Render Comparison Source # 
Instance details

Defined in Render.TypeChecking

Render NamedMeta Source # 
Instance details

Defined in Render.TypeChecking

Render Polarity Source # 
Instance details

Defined in Render.TypeChecking

Render Occurrence Source # 
Instance details

Defined in Render.TypeChecking

Render AbsolutePath Source # 
Instance details

Defined in Render.Position

Render CPUTime Source # 
Instance details

Defined in Render.Utils

Render Int32 Source # 
Instance details

Defined in Render.Class

Render Doc Source # 
Instance details

Defined in Render.Class

Render Integer Source # 
Instance details

Defined in Render.Class

Render Bool Source # 
Instance details

Defined in Render.Class

Render Int Source #

Other instances of Render

Instance details

Defined in Render.Class

Render a => Render (Arg a) Source #

Arg

Instance details

Defined in Render.Concrete

Render a => Render (MaybePlaceholder a) Source #

MaybePlaceholder

Instance details

Defined in Render.Concrete

Render a => Render (WithHiding a) Source # 
Instance details

Defined in Render.Concrete

Render a => Render (Binder' a) Source # 
Instance details

Defined in Render.Concrete

Render a => Render (FieldAssignment' a) Source # 
Instance details

Defined in Render.Concrete

Render (OpApp Expr) Source #

OpApp

Instance details

Defined in Render.Concrete

Render a => Render (Pattern' a) Source # 
Instance details

Defined in Render.Internal

Render a => Render (Substitution' a) Source # 
Instance details

Defined in Render.Internal

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 tm => Render (Elim' tm) Source # 
Instance details

Defined in Render.Internal

Render a => Render (Interval' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Render a => Render (Position' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Render a => Render (Range' (Maybe a)) Source # 
Instance details

Defined in Render.Position

Render c => Render (IPBoundary' c) Source #

IPBoundary'

Instance details

Defined in Render.Interaction

Render a => Render (List1 a) Source # 
Instance details

Defined in Render.Class

Render a => Render (List2 a) Source # 
Instance details

Defined in Render.Class

Render a => Render [a] Source # 
Instance details

Defined in Render.Class

Methods

render :: [a] -> Inlines Source #

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

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

OutputConstraint

Instance details

Defined in Render.Interaction

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

OutputForm

Instance details

Defined in Render.Interaction

(Render a, Render b) => Render (ImportDirective' a b) Source # 
Instance details

Defined in Render.Concrete

(Render a, Render b) => Render (ImportedName' a b) Source # 
Instance details

Defined in Render.Concrete

Render e => Render (Named NamedName e) Source #

Named NamedName (Named_)

Instance details

Defined in Render.Concrete

(Render a, Render b) => Render (Renaming' a b) Source # 
Instance details

Defined in Render.Concrete

(Render a, Render b) => Render (Using' a b) Source # 
Instance details

Defined in Render.Concrete

(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 a, Render b) => Render (Either a b) Source # 
Instance details

Defined in Render.Concrete

(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