Gabriel Ebner

The problem is that the `my_x` alias for `my_x x` is stored in the parser right now. A fix for this will probably have to wait until we implement #1674.

Is PR #1595 what you're looking for, or do you want something more sophisticated?

@leodemoura Some server and vscode integration is already there, see #1595. On the emacs side, it shouldn't be too hard to add a search command via helm. The most difficult...

> What would be the scope? Ideally, all the modules in the current package + dependencies (i.e. including the whole stdlib of course). Practically speaking, this probably means "all modules...

Damn, it was too good to be true... In any case, we should add this example as a test case (ok, just saw that you already added in the commit)....

Converting `(fun x _, ...) (unpack (pack a)) dummy` to `(fun x, ..) (unpack (pack a))` fixes this equation lemma. It works in all tests, except for the `non_exhaustive_error.lean` test,...

> here it fails because the minor hypothesis is the other way around?!? Just for the record, the arguments of the minor premise of the innermost eq.rec in the cases_on...

@leodemoura I understand that. I was referring to the "we did not have to agree on how the cases_on equational lemmas looked like."

> The traces can be quite long, and they are just sequences of strings. A further issue is that they are *one* string. There is really no way to separate...

> @gebner I am not very familiar with the log_tree code. However, it would be nice if we could store the trace objects there. We can basically store any kind...