Gabriel Ebner

The current plan is actually to remove this file altogether, @bryangingechen has started here: #288

Under the hood `pexpr` is exactly the same data structure as `expr`. The types are just there to help you not to confuse them (and e.g. call `infer_type` on a...

YES! YES! YES! If you open `src/tactic/lint/default.lean` in mathlib and write `#lint_all`, then you can already see the linting errors for the core library. IMHO we should change mathlib CI...

> To fix these, should we just start opening random linting PRs here or do we want to do something more systematic? If PRs are opened, they will be merged....

Now you know how old `prove_goal_async` is and how often it is used. :smile: Feel free to submit a PR adding `unfreeze_local_instances` if you want.

According to @alexpeattie, `realpath` isn't installed by default either. Can you shed some light on this, I don't have a mac? > realpath isn't installed on macOS by default either...

WTF? BTW, this doesn't work either: ```lean structure X : Type #check { X . } -- invalid structure instance, 'X' is not the name of a structure type ```

This doesn't work either: ```lean set_option old_structure_cmd true class A (α : Type). class B (α : Type) extends A α := (BB : ℕ) class C (α : Type)...

A more magic solution might be to set `module::scope_pos_info` in more places.

I feel obligated to mention that you could also implement `assumption?` in mathlib using [the trick described here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/set_option.20trace.2Esimplify.2Erewrite.20true/near/195957392).