You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
17 lines
447 B
Plaintext
17 lines
447 B
Plaintext
1 year ago
|
import Lake
|
||
|
|
open Lake DSL
|
||
|
|
|
||
|
|
package prova where
|
||
|
|
-- add package configuration options here
|
||
|
|
|
||
|
|
lean_lib Prova where
|
||
|
|
-- add library configuration options here
|
||
|
|
|
||
|
|
@[default_target]
|
||
|
|
lean_exe «prova» where
|
||
|
|
root := `Main
|
||
|
|
-- Enables the use of the Lean interpreter by the executable (e.g.,
|
||
|
|
-- `runFrontend`) at the expense of increased binary size on Linux.
|
||
|
|
-- Remove this line if you do not need such functionality.
|
||
|
|
supportInterpreter := true
|