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

11 lines
232 B
Lean4

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₂