monadt_with_IO/lakefile.lean

13 lines
248 B
Text
Raw Permalink Normal View History

2024-06-05 15:49:21 +09:00
import Lake
open Lake DSL
package «monadt_sample» where
-- add package configuration options here
lean_lib «MonadtSample» where
-- add library configuration options here
@[default_target]
lean_exe «monadt_sample» where
root := `Main