Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Abstract.Pretty

Synopsis

- showA :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String
- prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
- prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc
- showATop :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String
- prettyATop :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc
- prettyAUnqualify :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc

# Documentation

showA :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String Source #

prettyA :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc Source #

prettyAs :: (ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) => a -> m Doc Source #

showATop :: (ToConcrete a, Show (ConOfAbs a), MonadAbsToCon m) => a -> m String Source #

Variant of `showA` which does not insert outermost parentheses.

prettyATop :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc Source #

Variant of `prettyA` which does not insert outermost parentheses.

prettyAUnqualify :: (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) => a -> m Doc Source #

Variant of `prettyA` which unqualifies out-of-scope names.