lean4-htt/examples/helloDeps/foo/Foo.lean
2021-06-12 22:28:59 -04:00

7 lines
110 B
Text

import A
import B
import Foo.Bar
import Foo.Baz
def main : IO Unit :=
IO.println s!"Hello, {foo} {a} {b}!"