import Lake
open Lake DSL

package «ModuleName» where

@[default_target]
lean_lib «ModuleName» where
  roots := #[`ModuleName]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2"