8 lines
164 B
Text
8 lines
164 B
Text
import Lake
|
|
import Lean.Meta
|
|
open System Lake DSL
|
|
|
|
require hello from git
|
|
"https://github.com/leanprover/lake.git"@"master"/"examples"/"hello"
|
|
|
|
package git_hello
|