We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a2b605d commit 4c23923Copy full SHA for 4c23923
lakefile.toml
@@ -32,6 +32,8 @@ name = "FormalConjecturesForMathlib"
32
33
[[lean_lib]]
34
name = "FormalConjecturesTest"
35
+# Switch off warnings generated by `sorry`
36
+leanOptions = { warn.sorry = false }
37
38
39
name = "FormalConjectures"
0 commit comments