-
1
-
2
-
3
-
4
-
5
-
6
-
7
-
8
-
9
-
10
-
11
-
12
-
13
-
14
import Lake
open Lake DSL
package flean
lean_lib Flean
@[default_target]
lean_exe flean where
root := `Main
moreLinkArgs := #["-lsqlite3"]
require ffi from "ffi"
require batteries from git "https://github.com/leanprover-community/batteries" @ "main"