| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Translation.ReflectedToAbstract
Synopsis
- type Names = [Name]
- type WithNames a = ReaderT Names TCM a
- withName :: String -> (Name -> WithNames a) -> WithNames a
- askName :: Int -> WithNames (Maybe Name)
- class ToAbstract r a | r -> a where
- toAbstract :: r -> WithNames a
- toAbstract_ :: ToAbstract r a => r -> TCM a
- toAbstractWithoutImplicit :: ToAbstract r a => r -> TCM a
- mkDef :: QName -> TCM Expr
- mkSet :: Expr -> Expr
- toAbstractPats :: [Arg Pattern] -> WithNames (Names, [NamedArg Pattern])
Documentation
withName :: String -> (Name -> WithNames a) -> WithNames a Source #
Adds a new unique name to the current context.
askName :: Int -> WithNames (Maybe Name) Source #
Returns the name of the variable with the given de Bruijn index.
class ToAbstract r a | r -> a where Source #
Methods
toAbstract :: r -> WithNames a Source #
Instances
toAbstract_ :: ToAbstract r a => r -> TCM a Source #
Translate reflected syntax to abstract, using the names from the current typechecking context.
toAbstractWithoutImplicit :: ToAbstract r a => r -> TCM a Source #
Drop implicit arguments unless --show-implicit is on.