1 2 3 4 5 6 7 8 9 10 11 12 13
import Lake open Lake DSL package «lean-tui-test» where version := v!"0.1.0" require LeanPrism from "../lean-prism" -- local dev, no version lock require mathlib from git "https://github.com/leanprover-community/mathlib4.git" lean_lib Samples