lean
lean copied to clipboard
Add module_info.get_all
The motivation here is to teach doc-gen about empty default.lean files.
What's the easiest way to convert an std::vector<T> into a vm_obj holding a list? I was hoping to_obj had an overload for that.
I think vm_list.h is everything we have. Copy&pasted from to_obj(buffer<expr> const &):
vm_obj obj = mk_vm_nil();
for (unsigned i = ls.size(); i > 0; i--)
obj = mk_vm_cons(to_obj(ls[i - 1]), obj);
return obj;