module Agda.Syntax.Abstract.Pretty where

import Control.Applicative

import Agda.Syntax.Abstract
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Translation.AbstractToConcrete
import Agda.TypeChecking.Monad
import Agda.Utils.Pretty

showA :: (Show c, ToConcrete a c, MonadTCM tcm) => a -> tcm String
showA x = show <$> abstractToConcrete_ x

prettyA :: (Pretty c, ToConcrete a c, MonadTCM tcm) => a -> tcm Doc
prettyA x = pretty <$> abstractToConcrete_ x