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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-30 10:17:51 -08:00
parent 7cb566af15
commit 3bb0c18544
2 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/include/lean/lean.h generated
View file

@ -698,11 +698,6 @@ static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, uns
return o;
}
// TODO: delete
static inline lean_object * lean_alloc_ctor_big(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
return lean_alloc_ctor(tag, num_objs, scalar_sz);
}
static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) {
assert(i < lean_ctor_num_objs(o));
return lean_ctor_obj_cptr(o)[i];

1
stage0/src/include/lean/object.h generated
View file

@ -79,7 +79,6 @@ inline unsigned cnstr_num_objs(object * o) { return lean_ctor_num_objs(o); }
inline object ** cnstr_obj_cptr(object * o) { return lean_ctor_obj_cptr(o); }
inline uint8 * cnstr_scalar_cptr(object * o) { return lean_ctor_scalar_cptr(o); }
inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor(tag, num_objs, scalar_sz); }
inline obj_res alloc_cnstr_big(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor_big(tag, num_objs, scalar_sz); }
inline unsigned cnstr_tag(b_obj_arg o) { lean_assert(is_cnstr(o)); return lean_ptr_tag(o); }
inline void cnstr_set_tag(b_obj_arg o, unsigned tag) { lean_ctor_set_tag(o, tag); }
inline b_obj_res cnstr_get(b_obj_arg o, unsigned i) { return lean_ctor_get(o, i); }