Patrick Massot
Patrick Massot
This is also a somewhat global issue so I won't try to fix it right now. The behavior of `calc` in tactic mode changed recently, and I think we should...
The VSCode translations files actually has a [pretty active life](https://github.com/leanprover/vscode-lean/commits/master/translations.json) and I'm a bit worried that MIL contains many references to its current behavior. I'm not even sure it's currently...
This is a global issue hence I'm not doing anything about it in the PR I'm currently preparing. A lot of things were written back in the old days when...
As I wrote in an email, I think > On Zulip, you can helpfully specify that you are asking about the third exercise by referring to it as "the third...
This is built on top of #84. There is no point reviewing this before #84. With this PR, mypy no longer complains, even with options `--disallow-subclassing-any --disallow-untyped-defs`.
We need to update the hierarchy chapter to account for what happened in https://github.com/leanprover-community/mathlib4/pull/8386.
The crazy parentheses in the following snippet from Chapter 5 are probably either a mathport issue of working around a precedence bug that no longer exists. ```lean example (f :...
From Jireh [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/New.20chapter.20in.20MIL/near/398351301) about the groups and rings chapter: 1. Early on when discussing morphisms, the proofs used `f.map_mul` or `f.map_inv` as opposed to `map_mul f` and `map_inv f`....
In Chapter 5, we have ``` example : fac 0 = 1 := by simp [fac] ``` which is misleading since giving `[fac]` plays no role.