| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Translation.ReflectedToAbstract
- 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
- 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 Literal Expr Source | |
| ToAbstract Sort Expr Source | |
| ToAbstract Term Expr Source | |
| ToAbstract Pattern (Names, Pattern) Source | |
| ToAbstract (QNamed Clause) Clause Source | |
| ToAbstract [Arg Term] [NamedArg Expr] Source | |
| ToAbstract [QNamed Clause] [Clause] Source | |
| ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source | |
| ToAbstract r a => ToAbstract (Abs r) (a, Name) Source | |
| ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBindings Source | |
| ToAbstract (Expr, Elims) Expr Source | |
| ToAbstract (Expr, Elim) Expr Source | |
| ToAbstract r a => ToAbstract (Named name r) (Named name a) Source |
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.