Sebastian Ullrich

perf: garbage-collect dead sections

2

Benchmarks: https://github.com/leanprover/lean4/pull/1689#issuecomment-1268175703

Unexpected workspace symbol search results

3

Gonna use this issue to collect a few unexpected results I've encountered * searching for `smap` or `SMap` does not find the actual type

Make `trace.Elab.info` a proper message

1

We should move all `*Info.format` functions to `MessageData` instead so options like `pp.raw` and `pp.raw.showInfo` are heeded correctly.

Allow implicit auto-params

1

This came up in context of #1647: an implicit auto-param could only be specified using a named argument of `@`

As in Lean 3, declaration names starting with `_` should be rejected.

Double-backtick quotations with other syntax categories/parsers

2

Currently ``` ``(cat| ...) ``` is not supported, i.e. it can only be used with `command/term`. I'd like to wait with this change until we have unified the `|` notation...

Lack of smart unfolding was a feature

2

I had even mentioned it on our course slides! :)  For the sake of consistency with the base tactics, I would suggest: * `norm simp f` should do smart...

Rule suggestion: `elim *`

8

To get rid of the last item in https://github.com/IPDSnelting/tba-2022/blob/master/TBA/Util/AesopExts.lean. I assume this can be useful for forward reasoning with IHs in other projects as well. If the syntax looks agreeable,...