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

fix: exported symbol arities

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-05-28 15:48:41 -07:00 • committed by Sebastian Ullrich
parent fdad29770b
commit e5182fe4af
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/local_ctx.cpp
View file

@ -45,7 +45,7 @@ extern "C" object * lean_mk_empty_local_ctx(object*);
extern "C" object * lean_local_ctx_num_indices(object*);
extern "C" uint8 lean_local_ctx_is_empty(object*);
extern "C" object * lean_local_ctx_mk_local_decl(object * lctx, object * name, object * user_name, object * expr, uint8 bi);
extern "C" object * lean_local_ctx_mk_let_decl(object * lctx, object * name, object * user_name, object * type, object * value);
extern "C" object * lean_local_ctx_mk_let_decl(object * lctx, object * name, object * user_name, object * type, object * value, uint8 non_dep);
extern "C" object * lean_local_ctx_find(object * lctx, object * name);
extern "C" object * lean_local_ctx_erase(object * lctx, object * name);
@ -58,7 +58,7 @@ bool local_ctx::empty() const {
local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) {
unsigned idx = unbox(lean_local_ctx_num_indices(to_obj_arg()));
m_obj = lean_local_ctx_mk_let_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg());
m_obj = lean_local_ctx_mk_let_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg(), false);
return local_decl(idx, n, un, type, value);
}

2
src/runtime/io.cpp
View file

@ -736,7 +736,7 @@ extern "C" obj_res lean_io_wait(obj_arg t, obj_arg) {
return io_result_mk_ok(lean_task_get_own(t));
}
extern "C" obj_res lean_io_wait_any(b_obj_arg task_list) {
extern "C" obj_res lean_io_wait_any(b_obj_arg task_list, obj_arg) {
object * t = lean_io_wait_any_core(task_list);
object * v = lean_task_get(t);
lean_inc(v);