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;