lean4-htt/tests/playground/file.lean
2019-07-18 17:31:31 -07:00

3 lines
90 B
Text

def main : IO Unit :=
do contents ← IO.readTextFile "file.lean";
IO.println contents