Agda.Syntax.Translation.ReflectedToAbstract

Documentation

type Names = [Name]

type WithNames a = ReaderT Names TCM a

withName :: String -> (Name -> WithNames a) -> WithNames a

Adds a new unique name to the current context.

askName :: Int -> WithNames (Maybe Name)

Returns the name of the variable with the given de Bruijn index.

class ToAbstract r a | r -> a where

Minimal complete definition

toAbstract

Methods

toAbstract :: r -> WithNames a

Instances

ToAbstract Literal Expr

Methods

toAbstract :: Literal -> WithNames Expr

ToAbstract Sort Expr

Methods

toAbstract :: Sort -> WithNames Expr

ToAbstract Term Expr

Methods

toAbstract :: Term -> WithNames Expr

ToAbstract Pattern (Names, Pattern)

Methods

toAbstract :: Pattern -> WithNames (Names, Pattern)

ToAbstract (QNamed Clause) Clause

Methods

toAbstract :: QNamed Clause -> WithNames Clause

ToAbstract [Arg Term] [NamedArg Expr]

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract [QNamed Clause] [Clause]

Methods

toAbstract :: [QNamed Clause] -> WithNames [Clause]

ToAbstract r a => ToAbstract (Arg r) (NamedArg a)

Methods

toAbstract :: Arg r -> WithNames (NamedArg a)

ToAbstract r a => ToAbstract (Abs r) (a, Name)

Methods

toAbstract :: Abs r -> WithNames (a, Name)

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings

Methods

toAbstract :: (Dom r, Name) -> WithNames TypedBindings

ToAbstract (Expr, Elims) Expr

Methods

toAbstract :: (Expr, Elims) -> WithNames Expr

ToAbstract (Expr, Elim) Expr

Methods

toAbstract :: (Expr, Elim) -> WithNames Expr

ToAbstract r a => ToAbstract (Named name r) (Named name a)

Methods

toAbstract :: Named name r -> WithNames (Named name a)

toAbstract_ :: ToAbstract r a => r -> TCM a

Translate reflected syntax to abstract, using the names from the current typechecking context.

toAbstractWithoutImplicit :: ToAbstract r a => r -> TCM a

Drop implicit arguments unless --show-implicit is on.

mkSet :: Expr -> Expr

toAbstractPats :: [Arg Pattern] -> WithNames (Names, [NamedArg Pattern])