Skip to content

Make every Lean warning a compile error (warningAsError, like Tau Ceti) - #751

Open
Vilin97 wants to merge 3 commits into
mainfrom
vasil/warning-as-error
Open

Make every Lean warning a compile error (warningAsError, like Tau Ceti)#751
Vilin97 wants to merge 3 commits into
mainfrom
vasil/warning-as-error

Keep warning policy compatible with proof-length documentation

63a15b5
Select commit
Loading
Failed to load commit list.
Greptile Apps / Greptile Review succeeded Nov 6, 2026 in 1m 52s

Base review

Greptile has reviewed the Pull Request.

5 files reviewed, 0 comments added.

View more details on Greptile Apps