Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered



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.



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

Translate something in a context of the given precedence.

type AbsToCon = Reader EnvSource

We make the translation monadic for modularity purposes.

data DontTouchMe a Source


data Env Source