Agda.Syntax.Translation.AbstractToConcrete

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.

Documentation

class ToConcrete a where

Minimal complete definition

Nothing

Associated Types

type ConOfAbs a

Methods

toConcrete :: a -> AbsToCon (ConOfAbs a)

bindToConcrete :: a -> (ConOfAbs a -> AbsToCon b) -> AbsToCon b

Instances

ToConcrete BindName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName

Methods

toConcrete :: BindName -> AbsToCon (ConOfAbs BindName)

bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b

ToConcrete Declaration

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration

Methods

toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration)

bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b

ToConcrete Expr

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr

Methods

toConcrete :: Expr -> AbsToCon (ConOfAbs Expr)

bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon b

ToConcrete LHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS

Methods

toConcrete :: LHS -> AbsToCon (ConOfAbs LHS)

bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore)

bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding

Methods

toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding)

bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b

ToConcrete LetBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding

Methods

toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding)

bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b

ToConcrete ModuleApplication

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication)

bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b

ToConcrete Pattern

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern

Methods

toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern)

bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete RHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS

Methods

toConcrete :: RHS -> AbsToCon (ConOfAbs RHS)

bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b

ToConcrete SpineLHS

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS

Methods

toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS)

bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBinding

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding)

bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b

ToConcrete WhereDeclarations

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations

Methods

toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations)

bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b

ToConcrete ModuleName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName

Methods

toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName)

bindToConcrete :: ModuleName -> (ConOfAbs ModuleName -> AbsToCon b) -> AbsToCon b

ToConcrete Name

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name

Methods

toConcrete :: Name -> AbsToCon (ConOfAbs Name)

bindToConcrete :: Name -> (ConOfAbs Name -> AbsToCon b) -> AbsToCon b

ToConcrete QName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName

Methods

toConcrete :: QName -> AbsToCon (ConOfAbs QName)

bindToConcrete :: QName -> (ConOfAbs QName -> AbsToCon b) -> AbsToCon b

ToConcrete InteractionId

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId

Methods

toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId)

bindToConcrete :: InteractionId -> (ConOfAbs InteractionId -> AbsToCon b) -> AbsToCon b

ToConcrete AbstractName

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName

Methods

toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName)

bindToConcrete :: AbstractName -> (ConOfAbs AbstractName -> AbsToCon b) -> AbsToCon b

ToConcrete ResolvedName

Assumes name is not UnknownName.

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName

Methods

toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName)

bindToConcrete :: ResolvedName -> (ConOfAbs ResolvedName -> AbsToCon b) -> AbsToCon b

ToConcrete RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma)

bindToConcrete :: RangeAndPragma -> (ConOfAbs RangeAndPragma -> AbsToCon b) -> AbsToCon b

ToConcrete NamedMeta

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta

Methods

toConcrete :: NamedMeta -> AbsToCon (ConOfAbs NamedMeta)

bindToConcrete :: NamedMeta -> (ConOfAbs NamedMeta -> AbsToCon b) -> AbsToCon b

ToConcrete ()

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ()

Methods

toConcrete :: () -> AbsToCon (ConOfAbs ())

bindToConcrete :: () -> (ConOfAbs () -> AbsToCon b) -> AbsToCon b

ToConcrete Bool

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool

Methods

toConcrete :: Bool -> AbsToCon (ConOfAbs Bool)

bindToConcrete :: Bool -> (ConOfAbs Bool -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (Binder' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a)

Methods

toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a))

bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a)

Methods

toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a))

bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (Arg a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a)

Methods

toConcrete :: Arg a -> AbsToCon (ConOfAbs (Arg a))

bindToConcrete :: Arg a -> (ConOfAbs (Arg a) -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor)

Methods

toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor))

bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (Ranged a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Ranged a)

Methods

toConcrete :: Ranged a -> AbsToCon (ConOfAbs (Ranged a))

bindToConcrete :: Ranged a -> (ConOfAbs (Ranged a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (WithHiding a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a)

Methods

toConcrete :: WithHiding a -> AbsToCon (ConOfAbs (WithHiding a))

bindToConcrete :: WithHiding a -> (ConOfAbs (WithHiding a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (FieldAssignment' a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a)

Methods

toConcrete :: FieldAssignment' a -> AbsToCon (ConOfAbs (FieldAssignment' a))

bindToConcrete :: FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (IPBoundary' a)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a)

Methods

toConcrete :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a))

bindToConcrete :: IPBoundary' a -> (ConOfAbs (IPBoundary' a) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete (List1 a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a)

Methods

toConcrete :: List1 a -> AbsToCon (ConOfAbs (List1 a))

bindToConcrete :: List1 a -> (ConOfAbs (List1 a) -> AbsToCon b) -> AbsToCon b

ToConcrete (Maybe BindName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName)

Methods

toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName))

bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b

ToConcrete (Maybe Pattern)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern)

Methods

toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern))

bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b

ToConcrete (Maybe QName)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName)

Methods

toConcrete :: Maybe QName -> AbsToCon (ConOfAbs (Maybe QName))

bindToConcrete :: Maybe QName -> (ConOfAbs (Maybe QName) -> AbsToCon b) -> AbsToCon b

ToConcrete a => ToConcrete [a]

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs [a]

Methods

toConcrete :: [a] -> AbsToCon (ConOfAbs [a])

bindToConcrete :: [a] -> (ConOfAbs [a] -> AbsToCon b) -> AbsToCon b

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b)

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b))

bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon b0

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b)

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b))

bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon b0

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b)

Methods

toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b))

bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon b0

ToConcrete a => ToConcrete (Named name a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a)

Methods

toConcrete :: Named name a -> AbsToCon (ConOfAbs (Named name a))

bindToConcrete :: Named name a -> (ConOfAbs (Named name a) -> AbsToCon b) -> AbsToCon b

(ToConcrete a1, ToConcrete a2) => ToConcrete (Either a1 a2)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Either a1 a2)

Methods

toConcrete :: Either a1 a2 -> AbsToCon (ConOfAbs (Either a1 a2))

bindToConcrete :: Either a1 a2 -> (ConOfAbs (Either a1 a2) -> AbsToCon b) -> AbsToCon b

(ToConcrete a1, ToConcrete a2) => ToConcrete (a1, a2)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2)

Methods

toConcrete :: (a1, a2) -> AbsToCon (ConOfAbs (a1, a2))

bindToConcrete :: (a1, a2) -> (ConOfAbs (a1, a2) -> AbsToCon b) -> AbsToCon b

(ToConcrete a1, ToConcrete a2, ToConcrete a3) => ToConcrete (a1, a2, a3)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2, a3)

Methods

toConcrete :: (a1, a2, a3) -> AbsToCon (ConOfAbs (a1, a2, a3))

bindToConcrete :: (a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> AbsToCon b) -> AbsToCon b

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a)

Methods

toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a))

bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b

toConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)

Translate something in a context of the given precedence.

abstractToConcrete_ :: (ToConcrete a, MonadAbsToCon m) => a -> m (ConOfAbs a)

abstractToConcreteScope :: (ToConcrete a, MonadAbsToCon m) => ScopeInfo -> a -> m (ConOfAbs a)

abstractToConcreteHiding :: (LensHiding i, ToConcrete a, MonadAbsToCon m) => i -> a -> m (ConOfAbs a)

runAbsToCon :: MonadAbsToCon m => AbsToCon c -> m c

data RangeAndPragma

Constructors

RangeAndPragma Range Pragma

Instances

ToConcrete RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma)

bindToConcrete :: RangeAndPragma -> (ConOfAbs RangeAndPragma -> AbsToCon b) -> AbsToCon b

type ConOfAbs RangeAndPragma

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RangeAndPragma = Pragma

abstractToConcreteCtx :: (ToConcrete a, MonadAbsToCon m) => Precedence -> a -> m (ConOfAbs a)

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a

preserveInteractionIds :: AbsToCon a -> AbsToCon a

type MonadAbsToCon m = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc))

The function runAbsToCon can target any monad that satisfies the constraints of MonadAbsToCon.

data AbsToCon a

Instances

HasOptions AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pragmaOptions :: AbsToCon PragmaOptions

commandLineOptions :: AbsToCon CommandLineOptions

MonadReduce AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

liftReduce :: ReduceM a -> AbsToCon a

MonadStConcreteNames AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

runStConcreteNames :: StateT ConcreteNames AbsToCon a -> AbsToCon a

useConcreteNames :: AbsToCon ConcreteNames

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> AbsToCon ()

MonadTCEnv AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

askTC :: AbsToCon TCEnv

localTC :: (TCEnv -> TCEnv) -> AbsToCon a -> AbsToCon a

ReadTCState AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getTCState :: AbsToCon TCState

locallyTCState :: Lens' TCState a -> (a -> a) -> AbsToCon b -> AbsToCon b

withTCState :: (TCState -> TCState) -> AbsToCon a -> AbsToCon a

HasBuiltins AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getBuiltinThing :: SomeBuiltin -> AbsToCon (Maybe (Builtin PrimFun))

MonadAddContext AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

addCtx :: Name -> Dom Type -> AbsToCon a -> AbsToCon a

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> AbsToCon a -> AbsToCon a

updateContext :: Substitution -> (Context -> Context) -> AbsToCon a -> AbsToCon a

withFreshName :: Range -> ArgName -> (Name -> AbsToCon a) -> AbsToCon a

MonadDebug AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> AbsToCon String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

getVerbosity :: AbsToCon Verbosity

getProfileOptions :: AbsToCon ProfileOptions

isDebugPrinting :: AbsToCon Bool

nowDebugPrinting :: AbsToCon a -> AbsToCon a

MonadInteractionPoints AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

freshInteractionId :: AbsToCon InteractionId

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> AbsToCon ()

PureTCM AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasConstInfo AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getConstInfo :: QName -> AbsToCon Definition

getConstInfo' :: QName -> AbsToCon (Either SigError Definition)

getRewriteRulesFor :: QName -> AbsToCon RewriteRules

MonadFail AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fail :: String -> AbsToCon a

Applicative AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pure :: a -> AbsToCon a

(<*>) :: AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b

liftA2 :: (a -> b -> c) -> AbsToCon a -> AbsToCon b -> AbsToCon c

(*>) :: AbsToCon a -> AbsToCon b -> AbsToCon b

(<*) :: AbsToCon a -> AbsToCon b -> AbsToCon a

Functor AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fmap :: (a -> b) -> AbsToCon a -> AbsToCon b

(<$) :: a -> AbsToCon b -> AbsToCon a

Monad AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(>>=) :: AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b

(>>) :: AbsToCon a -> AbsToCon b -> AbsToCon b

return :: a -> AbsToCon a

MonadFresh NameId AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fresh :: AbsToCon NameId

MonadReader Env AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a

reader :: (Env -> a) -> AbsToCon a

Null (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

empty :: AbsToCon Doc

null :: AbsToCon Doc -> Bool

IsString (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fromString :: String -> AbsToCon Doc

Semigroup (AbsToCon Doc)

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(<>) :: AbsToCon Doc -> AbsToCon Doc -> AbsToCon Doc

sconcat :: NonEmpty (AbsToCon Doc) -> AbsToCon Doc

stimes :: Integral b => b -> AbsToCon Doc -> AbsToCon Doc

data Env

Instances

MonadReader Env AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a

reader :: (Env -> a) -> AbsToCon a

noTakenNames :: AbsToCon a -> AbsToCon a

lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName