    module Agda.Syntax.Abstract.Pretty where

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

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

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

    prettyAs :: (Pretty c, ToConcrete a [c]) => a -> TCM Doc
    prettyAs x = fsep . map pretty <$> abstractToConcrete_ x

    -- | Variant of 'showA' which does not insert outermost parentheses.

    showATop :: (Show c, ToConcrete a c) => a -> TCM String
    showATop x = show <$> abstractToConcreteCtx TopCtx x

    -- | Variant of 'prettyA' which does not insert outermost parentheses.

    prettyATop :: (Pretty c, ToConcrete a c) => a -> TCM Doc
    prettyATop x = pretty <$> abstractToConcreteCtx TopCtx x