batteries feat: `Fin.foldlM` and `Fin.foldrM`

feat: `Fin.foldlM` and `Fin.foldrM`

Open fgdorais opened this issue 1 year ago • 3 comments

May 29 '24 16:05 fgdorais

Might need minor adjustments after lean4#4304

May 29 '24 16:05 fgdorais

Git cleanup happened. @digama0's docstring correction was finally correctly applied.

Jun 06 '24 06:06 fgdorais

The basic definitions should eventually be moved to core but that can wait until there is less upstreaming pressure.

Jun 06 '24 06:06 fgdorais

Mathlib CI status (docs):

✅ Mathlib branch batteries-pr-testing-814 has successfully built against this PR. (2024-10-01 06:54:29) View Log

Oct 01 '24 06:10 leanprover-community-bot