1 2 3 4 5 6 7 8 9 10 11 12 13
import Lake open Lake DSL package covstream where require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.29.0" @[default_target] lean_lib Covstream where lean_exe covstream where root := `Main