Safe Haskell | None |
---|---|
Language | Haskell2010 |
Pretty printer for the concrete syntax.
Synopsis
- data SpecialCharacters = SpecialCharacters {}
- specialCharacters :: SpecialCharacters
- braces' :: Doc -> Doc
- dbraces :: Doc -> Doc
- forallQ :: Doc
- bracesAndSemicolons :: [Doc] -> Doc
- arrow :: Doc
- lambda :: Doc
- prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
- prettyRelevance :: LensRelevance a => a -> Doc -> Doc
- data NamedBinding = NamedBinding {}
- getLabel :: NamedArg a -> Maybe String
- isLabeled :: NamedArg BoundName -> Bool
- newtype Tel = Tel Telescope
- smashTel :: Telescope -> Telescope
- pRecord :: Name -> Maybe (Ranged Induction) -> Maybe HasEta -> Maybe (Name, IsInstance) -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc
- prettyOpApp :: forall a. Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
Documentation
data SpecialCharacters Source #
Picking the appropriate set of special characters depending on whether we are allowed to use unicode or have to limit ourselves to ascii.
bracesAndSemicolons :: [Doc] -> Doc Source #
prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc Source #
prettyHiding info visible doc
puts the correct braces
around doc
according to info info
and returns
visible doc
if the we deal with a visible thing.
prettyRelevance :: LensRelevance a => a -> Doc -> Doc Source #
data NamedBinding Source #
Instances
Pretty NamedBinding Source # | |
Defined in Agda.Syntax.Concrete.Pretty pretty :: NamedBinding -> Doc Source # prettyPrec :: Int -> NamedBinding -> Doc Source # prettyList :: [NamedBinding] -> Doc Source # |
pRecord :: Name -> Maybe (Ranged Induction) -> Maybe HasEta -> Maybe (Name, IsInstance) -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc Source #
prettyOpApp :: forall a. Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc] Source #