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

type Names = [Name] Source #

type WithNames a = ReaderT Names TCM a Source #

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 #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Literal -> WithNames Expr Source #
ToAbstract Sort Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Sort -> WithNames Expr Source #
ToAbstract Term Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Term -> WithNames Expr Source #
ToAbstract Pattern (Names, Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) Source #
ToAbstract (QNamed Clause) Clause Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract [QNamed Clause] [Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] Source #
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) Source #
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Abs r -> WithNames (a, Name) Source #
ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Dom r, Name) -> WithNames TypedBinding Source #
ToAbstract (Expr, Elims) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr Source #
ToAbstract (Expr, Elim) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr Source #
ToAbstract r a => ToAbstract (Named name r) (Named name a) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Named name r -> WithNames (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.

mkDef :: QName -> TCM Expr Source #

mkSet :: Expr -> Expr Source #

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