leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: decidableLE stack overflow


Arnav Sabharwal (Feb 16 2024 at 01:40):

While defining an instance ascribing to LinearOrder, defining decidableLE (even with 'sorry') leads to a stack overflow (uncaught exception) error. What could be the cause? Thanks!

Kevin Buzzard (Feb 16 2024 at 07:13):

#mwe ?

Arnav Sabharwal (Feb 18 2024 at 01:53):

So sorry didn't see this, the issue got resolved. LE.le was misbehaving.


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll