batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: Add `String.length_join` and `List.length_join`

Open tjf801 opened this issue 9 months ago • 3 comments

Quick fix for #770.

tjf801 avatar May 03 '24 04:05 tjf801

awaiting-review

tjf801 avatar May 03 '24 04:05 tjf801

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?

urkud avatar May 04 '24 02:05 urkud

Given that mathlib already has a List.length_join, we'll need to have a PR for mathlib that uses this branch of Std ready to go before this can be merged.

kim-em avatar May 06 '24 06:05 kim-em