Safe Haskell | None |
---|---|
Language | Haskell2010 |
- 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_ :: 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 #
toAbstract :: r -> WithNames a Source #
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.