Support optional sub rules in meta data converter syntax

[bvssvni]

I'm prototyping a proof assistant written in Dyon and discovered a weakness in the meta converter language:

  tactic := [name: str, forced: opt[bool]] =>
    {
      op:"tactic",
      name: name,
      forced: if forced == none() { false } else { unwrap(forced) },
      args: []
    };
  tactic_args := [name: str, forced: opt[bool], args <- args:"args"] =>
    {
      op:"tactic",
      name: name,
      forced: if forced == none() { false } else { unwrap(forced) },
      args: args
    };

Here I need two rules for tactics, one that has no arguments and one with arguments. I would like to have one rule for both cases.

Perhaps there is a way to make sub rules optional?

[bvssvni]

Could use the syntax args: opt <- args:"args".

• If : opt is not specified after the argument name, the sub rule is required
• If : opt is specified after the argument name, the sub rule is optional

This works well with Dyon syntax since opt defaults to opt[any].