lean4-htt/tests/playground/dir.lean
2019-07-25 18:12:44 -07:00

10 lines
232 B
Text

def main (xs : List String) : IO Unit :=
do
b₁ ← IO.isDir xs.head;
b₂ ← IO.fileExists xs.head;
d₁ ← IO.appDir;
d₂ ← IO.realPath ".";
IO.println b₁;
IO.println b₂;
IO.println d₁;
IO.println d₂