If we delegate everything to the meta-system, then we can use hugher order abstract syntax. And so define Lam as an constructor which takes an input a context. That is a function from term to term. So, in this case, you see you have a direct way of encoding a higher order abstract syntax representation of your system in this higher order metamodel | ![]() |