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

Safe HaskellNone

Agda.Syntax.Translation.AbstractToConcrete

Description

The translation of abstract syntax to concrete syntax has two purposes. First it allows us to pretty print abstract syntax values without having to write a dedicated pretty printer, and second it serves as a sanity check for the concrete to abstract translation: translating from concrete to abstract and then back again should be (more or less) the identity.

Synopsis

Documentation

toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c

Translate something in a context of the given precedence.

abstractToConcrete :: ToConcrete a c => Env -> a -> c

type AbsToCon = Reader Env

We make the translation monadic for modularity purposes.

data DontTouchMe a

Instances

data Env