The meta Phase

When it comes to actual code execution, there is no point to a definition without a body. Thus, in order to eagerly know what definitions might be executed at compile time and so need to be available including their bodies (in some executable shape), any definition used as an entry point to compile-time execution has to be tagged with the new meta modifier. This is automatically done in built-in metaprogramming syntax such as syntax, macro, and elab but may need to be done explicitly when manually applying metaprogramming attributes such as @[app_delab].

A meta definition may access (and thus invoke) other meta definitions only; a non-meta definition likewise may only access other non-meta definitions. For imported definitions, the meta marker can be added after the fact using meta import. meta importing a definition already in the meta phase leaves it in that phase. In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public meta definition in the current module: use public meta import or, if already meta, public import. This is usually the case, unless a definition was imported solely for use in local metaprograms.

module

meta import Std.Data.HashMap

local elab "my_elab" : command => do
  let m : Std.HashMap := {}
  ...

For convenience, meta also implies partial. This can be overridden by giving an explicit termination_by metric (such as one suggested by termination_by?), which may be necessary when the type of the definition is not known to be Nonempty.

As a guideline, it is usually preferable to apply meta as late as possible. Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. Only the final module(s) actually registering metaprograms then should use public meta import to import those helpers and define its metaprograms using built-in syntax like elab, using meta def, or using meta section.