From d4aab31ada10188f6268305bfe51e29aa53807f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Mar 2019 17:04:04 -0700 Subject: [PATCH] feat(library/init/io): `IO.userError` --- library/init/io.lean | 3 +++ 1 file changed, 3 insertions(+) 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"]