Yury G. Kudryashov
Yury G. Kudryashov
@kmill I tried your definition on current version of Lean4, then ```lean @[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c →...
What's so cool about `eglot` (never tried, so asking) that it beats Lean info view and orange bars?
Do you have Lean 3 mode installed?
Can you prepare a pull request? I guess, the less work you leave to maintainers, the higher the probability of getting it merged. What do other packages do about configurability...
Note that Mathlib has https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/List/Basic.html#List.length_join stated in terms of a generic `List.sum` instead of `Nat.sum`. What's the migration plan?
I changed some names and deduplicated lemmas while backporting, so review carefully, please.
awaiting-review
> > I changed some names and deduplicated lemmas while backporting, so review carefully, please. > > I'm not suggesting going back in this instance, but I think it is...
I've started doing the same changes in Mathlib, see leanprover-community/mathlib4#9738 for the first batch. Let's wait with merging this PR till I sync Mathlib with it. awaiting-author