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

chore: remove obsolete header

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-31 11:05:54 +02:00
parent 2215f93d14
commit b624b7d03f
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/include/lean/lean.h
View file

@ -1771,7 +1771,6 @@ static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
lean_ctor_set(r, 1, lean_box(0));
return r;
}
static inline lean_obj_res lean_mk_io_result(lean_obj_arg a) { return lean_io_result_mk_ok(a); }
static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
lean_object * r = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(r, 0, e);