Anand Rao
Anand Rao
Yes, I tested the above example and it does work under binders too.
Yes, it gave `enter [x, 1]` (as I chose to rewrite the left-hand side).
I will try to tackle this tomorrow.
> * For missing terminology such as the symmetric group, the best approach may be to add abbreviations with doc-strings. > > * In the longer run this can be...
- [ ] Integrate targeted formula translation with the overall translation set-up.
I'm facing this issue too; in my case, the match was sensitive to the order of the arguments, and swapping them allowed me to work around this bug. ``` import...
A metavariable for a `Level` created that way doesn't seem to play well with unification, so I was hoping that `argTyExpr` could somehow be defined as ``` let argTyExpr ←...
I happened to notice this issue just now, [Lean Auto](https://github.com/leanprover-community/lean-auto) might be another option to consider for automation (it depends on [Duper](https://github.com/leanprover-community/duper)).