Definable metas

[valis]

It may be convenient to be able define meta definitions in Arend code. For example, if we have a meta time that returns the current time and a meta print that prints its argument to stdout, we can implement a meta that runs some other meta and prints the time it took:

\meta runTimed m =>
  \let | t0 => time
       | result => m
       | t1 => time
  \in run {
    print (t1 - t0),
    result
  }

[ice1000]

Do we need to check termination for definable metas? Do we allow non-terminating definable metas?

[ice1000]

Do we even allow recursive definable metas?

[valis]

Do we need to check termination for definable metas? Do we allow non-terminating definable metas?

No

Do we even allow recursive definable metas?

Yes

[ice1000]

Fixed by #254