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

feat(util/object_ref): add ternary mk_cnstr

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-20 14:25:09 -07:00
parent 735aa57522
commit a2c2d1d9e7
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/object_ref.h
View file

@ -42,6 +42,10 @@ inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, unsigned scal
object * os[] = { o1, o2 };
return mk_cnstr(tag, 2, os, scalar_sz);
}
inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, object * o3, unsigned scalar_sz = 0) {
object * os[] = { o1, o2, o3 };
return mk_cnstr(tag, 3, os, scalar_sz);
}
/* The following definition is a low level hack that relies on the fact that sizeof(object_ref) == sizeof(object *). */
inline object_ref const & cnstr_obj_ref(object * o, unsigned i) {