Sebastian Ullrich
Sebastian Ullrich
> @Kha, another bug, where typeclass arguments that are included transitively can be included with multiplicity, apparently! > > Again on `lean-pr-testing-4814`, in `Mathlib.Order.Monotone`, we see: > > ``` >...
> Probably we ought to make the variable inclusion mechanism robust to this, and decline to include instance arguments if there are already there as implicit arguments. I'm a bit...
> failing with `failed to synthesize IsTrans N r`, despite both the arguments of `IsTrans` being mentioned in the theorem statement. Fixed > Here `include f` on `MulEquiv.decompositionMonoid` (or just...
> I think it would be better to just remove the indentation. If indentation is not desired in actual code, why would should it be included in these examples. It...
Note, `section.md` should be adjusted correspondingly. Perhaps we should merge them even?
@nomeata I can't reproduce any of these on master anymore, apparently some `decreasing_by` changes fixed them?
My fault, I can see it now
@digama0 I added a Lean version string field and hope this is now enough .olean metadata for the next decade :) . Could you take a look?
@digama0 @eric-wieser Final Comment Period :)
I won't worry about #2908 for now, given that it's only relevant for non-standard Lean builds now