| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Concrete.Pretty
Contents
Description
Pretty printer for the concrete syntax.
Synopsis
- attributesForModality :: HasOptions m => Modality -> m Doc
- bracesAndSemicolons :: Foldable t => t Doc -> Doc
- isLabeled :: NamedArg Binder -> Maybe ArgName
- pHasEta0 :: HasEta0 -> Doc
- pRecord :: Erased -> Name -> [RecordDirective] -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc
- pRecordDirective :: RecordDirective -> Doc
- prettyFiniteness :: BoundName -> Doc -> Doc
- prettyOpApp :: Pretty a => Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc]
- prettyTactic :: BoundName -> Doc -> Doc
- prettyTactic' :: TacticAttribute -> Doc -> Doc
- smashTel :: Telescope -> Telescope
- data NamedBinding = NamedBinding {}
- newtype Tel = Tel Telescope
- module Agda.Syntax.Concrete.Glyph
Documentation
attributesForModality :: HasOptions m => Modality -> m 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.
pRecord :: Erased -> Name -> [RecordDirective] -> [LamBinding] -> Maybe Expr -> [Declaration] -> Doc Source #
prettyOpApp :: Pretty a => Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Doc] Source #
prettyTactic' :: TacticAttribute -> Doc -> Doc Source #
data NamedBinding Source #
Constructors
| NamedBinding | |
Fields
| |
Instances
| Pretty NamedBinding Source # | |
Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: NamedBinding -> Doc Source # prettyPrec :: Int -> NamedBinding -> Doc Source # prettyList :: [NamedBinding] -> Doc Source # | |
module Agda.Syntax.Concrete.Glyph