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



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.

abstractToConcrete_ :: (MonadTCM tcm, ToConcrete a c) => a -> tcm cSource

runAbsToCon :: MonadTCM tcm => AbsToCon a -> tcm aSource

type AbsToCon = Reader EnvSource

We make the translation monadic for modularity purposes.

data DontTouchMe a Source


data Env Source