Gabriel Ebner

bors try

bors try

I think for the `?` notation to work, you need to add this before `assumption`: (copied from `rcases`) ```lean precedence `?`:max ``` You should also add an `assumption'` tactic (of...

If you write `. assumption` after the type of an argument, then Lean will try to automatically fill in the argument by calling the tactic `assumption`. This is also works...

I think you should add an `assumption''` and use that in the tests. bors try

Oh wow, the precedence change broke a lot of stuff. You should post a message on Zulip about this. I'm not sure what the correct solution here is.

I think `vm_list.h` is everything we have. Copy&pasted from `to_obj(buffer const &)`: ```c++ vm_obj obj = mk_vm_nil(); for (unsigned i = ls.size(); i > 0; i--) obj = mk_vm_cons(to_obj(ls[i -...

It's too late now, but it's ok to make `leanpkg` meta. There's nothing we gain from it being non-meta.

> iterate', compare iterate in init.meta.tactic. They do different things. > guard_target' uses guard_expr_eq', whereas guard_target uses guard_expr_eq. :-1: This is mainly used for testing, where you explicitly do not...

Access to `/proc` is required because lean needs to determine the absolute path of the executable (in order to find the core library path). The error message should be better...