Bryan Gin-ge Chen
Bryan Gin-ge Chen
> 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. [Here's a gist](https://gist.github.com/bryangingechen/6c2f397b14d756c3c7f72440cd9b4816) based on a recent mathlib...
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/linting.20the.20core.20library/near/195738547).
Could you add some tests showing the desired new behavior?
There are a few types of tests: - Lean files in [`tests/lean`](https://github.com/leanprover-community/lean/tree/master/tests/lean) should generate the corresponding `.lean.expected.out` file. - Lean files in [`tests/lean/run`](https://github.com/leanprover-community/lean/tree/master/tests/lean/run) should run without creating any output -...
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Porting.20Lean.20code.20to.20Lean.203.2E17.2E0)
Is it possible to display not just the first goal, but all goals? ```lean example : true ∧ true ∧ true := by split; split; trivial -- ^ 1 goal:\n⊢...
Thanks Mario, that makes better sense.
Removing the need to add `using_well_founded` everywhere would be great. `def_replacer` is in mathlib though, so what should we do here? Is there a set up somewhere I can refer...
@fpvandoorn Ah, cool! Do you mind making a PR to core either replacing `generalize` with `generalize'` or just fixing it?
Thanks, I crossed those out in the post above!