\module Meta
Scope metas
Meta using
, usingOnly
and hiding
controls the scope.
using (e_1, ... e_n) e
addse_1
, …e_n
to the context before checkinge
.using (e_1, ... e_n)
is sometimes used in other context-manipulating metas, that addse_1
, …e_n
to the context it uses.usingOnly (e_1, ... e_n) e
replaces the context withe_1
, …e_n
before checkinge
.usingOnly (e_1, ... e_n)
is sometimes used in other context-manipulating metas, that replaces the context is uses withe_1
, …e_n
.hiding (e_1, ... e_n) e
hides local bindingse_1
, …e_n
from the context before checkinge
.hiding (e_1, ... e_n)
is sometimes used in other context-manipulating metas, that hidese_1
, …e_n
from the context it uses.