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

Render.Common

Synopsis

Documentation

renderHiding :: LensHiding a => a -> (Inlines -> Inlines) -> Inlines -> Inlines Source #

From prettyHiding renderHiding info visible text puts the correct braces around text according to info info and returns visible text if the we deal with a visible thing.

renderRelevance :: LensRelevance a => a -> Inlines -> Inlines Source #

renderQuantity :: LensQuantity a => a -> Inlines -> Inlines Source #

renderCohesion :: LensCohesion a => a -> Inlines -> Inlines Source #

Orphan instances

Render Cohesion Source # 
Instance details

Methods

render :: Cohesion -> Inlines Source #

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

Render Induction Source # 
Instance details

Methods

render :: Induction -> Inlines Source #

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

Render MetaId Source #

MetaId

Instance details

Methods

render :: MetaId -> Inlines Source #

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

Render NameId Source #

NameId

Instance details

Methods

render :: NameId -> Inlines Source #

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

Render Quantity Source #

Quantity

Instance details

Methods

render :: Quantity -> Inlines Source #

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

Render QωOrigin Source # 
Instance details

Methods

render :: QωOrigin -> Inlines Source #

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

Render Relevance Source #

Relevance

Instance details

Methods

render :: Relevance -> Inlines Source #

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

(Render p, Render e) => Render (RewriteEqn' qn nm p e) Source # 
Instance details

Methods

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

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