max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/io): IO.userError

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-22 17:04:04 -07:00
parent c10a99e96f
commit d4aab31ada
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/io.lean
View file

@ -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"]