lean icon indicating copy to clipboard operation
lean copied to clipboard

Add module_info.get_all

Open eric-wieser opened this issue 2 years ago • 2 comments

The motivation here is to teach doc-gen about empty default.lean files.

eric-wieser avatar Nov 02 '21 09:11 eric-wieser

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.

eric-wieser avatar Nov 04 '21 11:11 eric-wieser

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;

gebner avatar Nov 04 '21 13:11 gebner