Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Pretty printer for the concrete syntax.
Synopsis
- newtype Tel = Tel Telescope
- data NamedBinding = NamedBinding {}
- prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
- prettyRelevance :: LensRelevance a => a -> Doc -> Doc
- bracesAndSemicolons :: Foldable t => t Doc -> Doc
- prettyQuantity :: LensQuantity a => a -> Doc -> Doc
- prettyErased :: Erased -> Doc -> Doc
- prettyCohesion :: LensCohesion a => a -> Doc -> Doc
- prettyTactic :: BoundName -> Doc -> Doc
- prettyTactic' :: TacticAttribute -> Doc -> Doc
- prettyFiniteness :: BoundName -> Doc -> Doc
- attributesForModality :: Modality -> Doc
- prettyOpApp :: forall a. Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc]
- smashTel :: Telescope -> Telescope
- isLabeled :: NamedArg Binder -> Maybe ArgName
- pRecord :: Name -> RecordDirectives -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc
- pRecordDirective :: RecordDirective -> Doc
- pHasEta0 :: HasEta0 -> Doc
- module Agda.Syntax.Concrete.Glyph
Documentation
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 # |
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 #
prettyQuantity :: LensQuantity a => a -> Doc -> Doc Source #
prettyCohesion :: LensCohesion a => a -> Doc -> Doc Source #
prettyTactic' :: TacticAttribute -> Doc -> Doc Source #
attributesForModality :: Modality -> Doc Source #
Show the attributes necessary to recover a modality, in long-form (e.g. using at-syntax rather than dots). For the default modality, the result is at-ω (rather than the empty document). Suitable for showing modalities outside of binders.
prettyOpApp :: forall a. Pretty a => QName -> [NamedArg (MaybePlaceholder a)] -> [Doc] Source #
pRecord :: Name -> RecordDirectives -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc Source #
module Agda.Syntax.Concrete.Glyph