Error with meta mutual defs

[digama0]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

meta mutual def causes the error unexpected error, failed to generate equational lemmas in the front-end. Example:

meta mutual def X, Y
with X : nat → nat | n := 0
with Y : nat → nat | n := 0

Presumably the correct behavior is to not attempt to generate equational lemmas at all, since it is a meta definition.

Versions

Lean v3.4.0 (commit 4be96ea)