Error with meta mutual defs - Githubissues

leanprover / lean3

Lean Theorem Prover

http://leanprover.github.io/

Apache License 2.0

2.15k stars 217 forks source link

Error with meta mutual defs #1957

Open digama0 opened 6 years ago

digama0 commented 6 years ago

Prerequisites

[X] 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 4be96eaa)