Safe Haskell	None
Language	Haskell2010

FreeC.Backend.Coq.Pretty

Contents

Orphan instances

Description

This module contains a Pretty instance for nodes of the Coq AST.

Since we want to have a pretty instance for all Gallina instances but want to avoid overlapping instances, there is a wrapper type PrettyCoq. To pretty print a node x of the Coq AST you can write pretty (PrettyCoq x).

There are instances for the actual node of commonly pretty printed types of nodes.

Synopsis

newtype PrettyCoq a = PrettyCoq {
- unPrettyCoq :: a
}
prettyCoq :: Gallina a => a -> Doc

Documentation

newtype PrettyCoq a Source #

Wrapper data type that makes a Coq AST node of type a pretty printable.

Constructors

PrettyCoq
Fields unPrettyCoq :: a

Instances

Gallina a => Pretty (PrettyCoq a) Source #

Pretty instance for nodes of the Coq AST.

When pretty printing a list of nodes, the individual documents are concatenated with newlines.

Instance details

Defined in FreeC.Backend.Coq.Pretty

Methods

pretty :: PrettyCoq a -> Doc #

prettyList :: [PrettyCoq a] -> Doc #

prettyCoq :: Gallina a => a -> Doc Source #

Pretty prints the given Coq AST node.

Orphan instances

Pretty Sentence Source #	Sentences often need to be pretty printed in the tests and when writing the generated Coq code to the console or a file.
Instance details Methods pretty :: Sentence -> Doc # prettyList :: [Sentence] -> Doc #
Pretty Term Source #	Terms often need to be pretty printed in the tests.
Instance details Methods pretty :: Term -> Doc # prettyList :: [Term] -> Doc #