lean4-htt/tests/lean/stdio.lean
2020-09-30 07:05:46 -07:00

31 lines
783 B
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

new_frontend
open IO.FS
def usingIO {α} (x : IO α) := x
#eval usingIO do
let out ← IO.getStdout;
(out.putStrLn "print stdout" : IO Unit)
#eval usingIO do
let err ← IO.getStderr;
(err.putStr "print stderr" : IO Unit)
open usingIO IO
def test : IO Unit := do
FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do
{ let h₂ ← FS.Handle.mk "stdout2.txt" IO.FS.Mode.write;
withStdout (Stream.ofHandle h₁) $ do
println "line 1";
«catch»
( do
withStdout (Stream.ofHandle h₂) $ println "line 2";
throw $ IO.userError "my error" )
( fun e => println e );
println "line 3" };
println "line 4";
println "\n> stdout1.txt";
readFile "stdout1.txt" >>= print;
println "\n> stdout2.txt";
readFile "stdout2.txt" >>= print
#eval test