Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Translation.AbstractToConcrete

Description

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.

Synopsis

Documentation

class ToConcrete a where Source #

Minimal complete definition

Nothing

Associated Types

type ConOfAbs a Source #

Methods

toConcrete :: a -> AbsToCon (ConOfAbs a) Source #

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

Instances

Instances details
ToConcrete Bool Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool Source #

Methods

toConcrete :: Bool -> AbsToCon (ConOfAbs Bool) Source #

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

ToConcrete () Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs () Source #

Methods

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

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

ToConcrete InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId Source #

Methods

toConcrete :: InteractionId -> AbsToCon (ConOfAbs InteractionId) Source #

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

ToConcrete NamedMeta Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta Source #

Methods

toConcrete :: NamedMeta -> AbsToCon (ConOfAbs NamedMeta) Source #

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

ToConcrete ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName Source #

Methods

toConcrete :: ModuleName -> AbsToCon (ConOfAbs ModuleName) Source #

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

ToConcrete QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName Source #

Methods

toConcrete :: QName -> AbsToCon (ConOfAbs QName) Source #

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

ToConcrete Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name Source #

Methods

toConcrete :: Name -> AbsToCon (ConOfAbs Name) Source #

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

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName Source #

Methods

toConcrete :: ResolvedName -> AbsToCon (ConOfAbs ResolvedName) Source #

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

ToConcrete AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName Source #

Methods

toConcrete :: AbstractName -> AbsToCon (ConOfAbs AbstractName) Source #

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

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

Methods

toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source #

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

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

Methods

toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source #

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

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

Methods

toConcrete :: LHS -> AbsToCon (ConOfAbs LHS) Source #

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

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

Methods

toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source #

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

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

Methods

toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source #

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

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

Methods

toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source #

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

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

Methods

toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source #

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

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding Source #

Methods

toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source #

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

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding Source #

Methods

toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source #

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

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication Source #

Methods

toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source #

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

ToConcrete Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration Source #

Methods

toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration) Source #

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

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr Source #

Methods

toConcrete :: Expr -> AbsToCon (ConOfAbs Expr) Source #

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

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName Source #

Methods

toConcrete :: BindName -> AbsToCon (ConOfAbs BindName) Source #

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

ToConcrete RangeAndPragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma Source #

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma) Source #

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

ToConcrete a => ToConcrete [a] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs [a] Source #

Methods

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

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

ToConcrete (Maybe QName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName) Source #

Methods

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

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

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

Methods

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

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

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

Methods

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

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

ToConcrete a => ToConcrete (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a) Source #

Methods

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

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

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

Methods

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

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

ToConcrete a => ToConcrete (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a) Source #

Methods

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

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

ToConcrete a => ToConcrete (WithHiding a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a) Source #

Methods

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

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

ToConcrete a => ToConcrete (FieldAssignment' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a) Source #

Methods

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

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

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) Source #

Methods

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

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

ToConcrete a => ToConcrete (Binder' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) Source #

Methods

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

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

ToConcrete a => ToConcrete (IPBoundary' a) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a) Source #

Methods

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

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

(ToConcrete a1, ToConcrete a2) => ToConcrete (Either a1 a2) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Either a1 a2) Source #

Methods

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

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

(ToConcrete a1, ToConcrete a2) => ToConcrete (a1, a2) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2) Source #

Methods

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

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

ToConcrete a => ToConcrete (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a) Source #

Methods

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

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

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b) Source #

Methods

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

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

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b) Source #

Methods

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

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

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b) Source #

Methods

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

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

(ToConcrete a1, ToConcrete a2, ToConcrete a3) => ToConcrete (a1, a2, a3) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2, a3) Source #

Methods

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

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

(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) Source #

Methods

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

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

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

Translate something in a context of the given precedence.

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

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

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

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

data RangeAndPragma Source #

Constructors

RangeAndPragma Range Pragma 

Instances

Instances details
ToConcrete RangeAndPragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma Source #

Methods

toConcrete :: RangeAndPragma -> AbsToCon (ConOfAbs RangeAndPragma) Source #

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

type ConOfAbs RangeAndPragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs RangeAndPragma = Pragma

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

withScope :: ScopeInfo -> AbsToCon a -> AbsToCon a Source #

preserveInteractionIds :: AbsToCon a -> AbsToCon a Source #

type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m) Source #

We need: - Read access to the AbsToCon environment - Read access to the TC environment - Read access to the TC state - Read and write access to the stConcreteNames part of the TC state - Read access to the options - Permission to print debug messages

data AbsToCon a Source #

Instances

Instances details
Monad AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

return :: a -> AbsToCon a #

Functor AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

MonadFail AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fail :: String -> AbsToCon a #

Applicative AbsToCon Source # 
Instance details

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 #

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

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

getVerbosity :: AbsToCon Verbosity Source #

isDebugPrinting :: AbsToCon Bool Source #

nowDebugPrinting :: AbsToCon a -> AbsToCon a Source #

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pragmaOptions :: AbsToCon PragmaOptions Source #

commandLineOptions :: AbsToCon CommandLineOptions Source #

MonadTCEnv AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

askTC :: AbsToCon TCEnv Source #

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

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

runStConcreteNames :: StateT ConcreteNames AbsToCon a -> AbsToCon a Source #

useConcreteNames :: AbsToCon ConcreteNames Source #

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

ReadTCState AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getTCState :: AbsToCon TCState Source #

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

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

HasBuiltins AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

getBuiltinThing :: String -> AbsToCon (Maybe (Builtin PrimFun)) Source #

MonadReader Env AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env #

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

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

data Env Source #

Instances

Instances details
MonadReader Env AbsToCon Source # 
Instance details

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 Source #

lookupQName :: AllowAmbiguousNames -> QName -> AbsToCon QName Source #