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

fix: we cannot export constants

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-23 11:54:54 -07:00
parent 4296e1d83e
commit 918256ff1f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/System/IOError.lean
View file

@ -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 :=