import Lake
open Lake DSL

package starG where
  leanOptions := #[
    ⟨`autoImplicit, false⟩
  ]

-- Mathlib lives at ../../mathlib4 (i.e. C:/lrc/mathlib4), shared across all
-- sibling Lean projects under C:/lrc (q-DQ, PWK, lean-dequantization-template,
-- etc.). The build artifacts in ../../mathlib4/.lake are reused by every
-- project that points at this path. To bootstrap once:
--
--     git clone https://github.com/leanprover-community/mathlib4 ../../mathlib4
--     cd ../../mathlib4 && lake exe cache get
--
-- If you'd rather pull a per-project copy of mathlib via git, replace the
-- line below with `require mathlib from git "https://github.com/leanprover-community/mathlib4"`.
require mathlib from "../../mathlib4"

@[default_target]
lean_lib StarG