lakefile

   1import Lake
   2open Lake DSL
   3
   4package «shape-of-logic» where
   5  leanOptions := #[
   6    ⟨`autoImplicit, false⟩
   7  ]
   8
   9require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
  10
  11lean_lib IndisputableMonolith where
  12  roots := #[`IndisputableMonolith]
  13