Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Formalizing the proof of PFR in Lean4 using Blueprint: a short tour. Parent comment
In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.
There are no comments on this comment yet.
In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.