diff --git a/library/init/io.lean b/library/init/io.lean index ec721c5ba1..1b00e305d1 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -30,6 +30,9 @@ like in https://doc.rust-lang.org/std/IO/enum.ErrorKind.html @[derive HasToString Inhabited] def IO.error := String +def IO.userError (s : String) : IO.error := +s + abbrev IO : Type → Type := EIO IO.error @[extern "lean_io_unsafe"]