You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
Description
The following MWE causes a stack overflow in lake build or causes the LSP to hang
inductive A
| foo : A → A
inductive B : A → A → Type where
| foo : B (.foo q) q
structure ImageR (R : α → α → Type) (a : α) where
{b : α}
(r : R a b)
instance : Ord (ImageR B p) where
compare i j := match i.r with
| .foo => match j.r with
| .foo => sorry
Steps to Reproduce
Put this snippet in a lean project
lake build
Expected behavior: No stack overflow Actual behavior: Stack overflow
Versions
[Output of #eval Lean.versionString or of lean --version in the folder that the issue occured in] 4.7.0-rc2
[OS version] NixOS 24.05pre-git (Uakari) x86_64
The text was updated successfully, but these errors were encountered:
Prerequisites
Description
The following MWE causes a stack overflow in
lake build
or causes the LSP to hangSteps to Reproduce
lake build
Expected behavior: No stack overflow
Actual behavior: Stack overflow
Versions
[Output of
#eval Lean.versionString
or oflean --version
in the folder that the issue occured in] 4.7.0-rc2[OS version] NixOS 24.05pre-git (Uakari) x86_64
The text was updated successfully, but these errors were encountered: