31 lines
931 BLFS
Lean4
31 lines
931 BLFS
Lean4
import Lake
|
||
open Lake DSL
|
||
|
||
package math2001 where
|
||
moreServerArgs := #[
|
||
"-Dlinter.unusedVariables=false", -- ignores unused variables
|
||
"-DquotPrecheck=false",
|
||
"-DwarningAsError=false",
|
||
"-Dpp.unicode.fun=true" -- pretty-prints `fun a ↦ b`
|
||
]
|
||
|
||
lean_lib Library
|
||
|
||
@[default_target]
|
||
lean_lib Math2001 where
|
||
moreLeanArgs := #[
|
||
"-Dlinter.unusedVariables=false", -- ignores unused variables
|
||
"-DquotPrecheck=false",
|
||
"-DwarningAsError=false",
|
||
"-Dpp.unicode.fun=true" -- pretty-prints `fun a ↦ b`
|
||
]
|
||
|
||
/-
|
||
want also
|
||
"-Dpush_neg.use_distrib=true", -- negates ¬(P ∧ Q) to (¬ P ∨ ¬ Q)
|
||
but currently only Lean core options can be set in lakefile
|
||
-/
|
||
|
||
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "750b7536599c7b0924e12fe79d0522b8554125c9"
|
||
require autograder from git "https://github.com/robertylewis/cs22-lean-autograder" @ "1c6119111649e9c18594be3b3722836025a96e86"
|