📦 hediet / lean-experiments

lean-experiments / lakefile.lean
📄 lakefile.lean · 15 lines 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15import Lake
open Lake DSL

package «lean-playground» where
  -- add package configuration options here

lean_lib «LeanPlayground» where
  -- add library configuration options here

@[default_target]
lean_exe «hello» where
  root := `Main

require mathlib from git "https://github.com/leanprover-community/mathlib4"