Timeline for A well-founded relation on lists
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 24, 2022 at 14:44 | comment | added | Peter LeFanu Lumsdaine | @JunyanXu : Thanks for the pingback — very happy to hear this turned out useful, and nice to see it formalised! | |
| May 17, 2022 at 17:21 | comment | added | Junyan Xu |
Thanks for posting the proof. It has now been formalized in Lean: github.com/leanprover-community/mathlib/pull/14190/…. Notice that acc (<) x in Lean means that the non-strict slice $X/x$ is well-founded.
|
|
| Jan 23, 2016 at 10:20 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 3.0 |