Meta definitions

Meta definitions are usually defined externally in Java code, but it is also possible to describe simple metas directly in Arend code. The general syntax of such a meta looks like this:

\meta f x_1 ... x_n => e

where f is a name, x_1, … x_n are names of parameters, and e is an expression. This expression is typechecked only when the meta is invoked. It expects n arguments and f e_1 … e_n is replaced with e[e_1/x_1, … e_n/x_n] and this expression is typechecked instead of the original application.