Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Translation.ReflectedToAbstract

Synopsis

Documentation

type Names = [Name] Source #

withName :: MonadReflectedToAbstract m => String -> (Name -> m a) -> m a Source #

Adds a new unique name to the current context.

askName :: MonadReflectedToAbstract m => Int -> m (Maybe Name) Source #

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

class ToAbstract r a | r -> a where Source #

Instances

Instances details
ToAbstract Literal Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract Pattern (Names, Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract [Arg Term] [NamedArg Expr] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract [QNamed Clause] [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Abs r -> m (a, Name) Source #

ToAbstract r Expr => ToAbstract (Dom r, Name) TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (Expr, Elims) Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract (Expr, Elim) Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

ToAbstract r a => ToAbstract (Named name r) (Named name a) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Named name r -> m (Named name a) Source #

toAbstract_ :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a Source #

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

toAbstractWithoutImplicit :: (ToAbstract r a, MonadFresh NameId m, MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) => r -> m a Source #

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