lean4-htt/lakefile.lean
2022-10-20 12:20:57 -04:00

11 lines
155 B
Text

import Lake.DSL
open System Lake DSL
package lake
lean_lib Lake
@[default_target]
lean_exe lake where
root := `Lake.Main
supportInterpreter := true