issue !4#10741: simp[LE.le] causes Lean server to crash

Stream: triage

[Random Issue Bot]

Today I chose issue 10741 for discussion!

simp[LE.le] causes Lean server to crash
Created by @None (@Arnav-99) on 2024-02-20
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 10741 for discussion!

simp[LE.le] causes Lean server to crash
Created by @None (@Arnav-99) on 2024-02-20
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

On a recent mathlib this now seems to give

tactic 'simp' failed, nested error:
maximum recursion depth has been reached

which is perhaps less surprising.