From 918256ff1f55cd60a4c4dab5518b6d004a899fec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Mar 2020 11:54:54 -0700 Subject: [PATCH] fix: we cannot export constants --- src/Init/System/IOError.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index e97905f1d8..9696c4e412 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -59,7 +59,7 @@ IO.Error.userError s namespace IO.Error @[export lean_mk_io_error_eof] -def mkEofError : IO.Error := unexpectedEof +def mkEofError : Unit → IO.Error := fun _ => unexpectedEof @[export lean_mk_io_error_inappropriate_type_file] def mkInappropriateTypeFile : String → UInt32 → String → IO.Error :=