Leopold Fajtak
5 lines
85 B
Lean4
5 lines
85 B
Lean4
import InductiveVerification
|
|
|
|
def main : IO Unit :=
|
|
IO.println s!"Hello, {hello}!"
|