Crash

Stream: lean4

[Yury G. Kudryashov]

Lean crashed on https://github.com/leanprover-community/mathlib4/blob/e385b3de0af88d5b4f3cfb44fea9cd26c6065205/Mathlib/GroupTheory/Submonoid/Basic.lean with error message

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:849:14: unknown metavariable
(backtrace)

This is a WIP branch and I didn't start fixing this file yet but I assume that crashes should be reported anyway.

[Kim Morrison]

Unfortunately unless you (or anyone else!) has the enthusiasm to make a Mathlib free example of this, it's unlikely we can do anything with this report.

[Kevin Buzzard]

Yury, I looked at trying to fix this issue but as well as the crash there seemed to be 100+ errors in that file; this put me off trying to minimise.

[Yury G. Kudryashov]

Yes, this is a file I didn't start to migrate to the new API. I'll try to minimise later this week.