James Gallicchio

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Monadic.20array.20init/near/436387474

Refactor operations

1

Big refactor of `Ops.lean`. - Improves class names to be consistent/predictable - Refactors `Fold` correctness to be in terms of `ToMultiset` instead of list permutations. This includes some lemmas about...

Map operation class

3

`Functor` only applies to type constructors (`Type u -> Type v`). So, is insufficient for a general purpose `map : (A -> B) -> CA -> CB` where perhaps `CA`...

it is getting too big. split it.

This adds support for ranges over types other than `Nat`.

As in title. ``` set_option pp.universes true #check IndexType.card (Prod (Fin 2) (Fin 2)) -- IndexType.card.{0, u_1} (Prod.{0, 0} (Fin 2) (Fin 2)) ``` Probably we should not require `Fold`...

A husk of a PR. These are going to take a lot of work to prove correct. Depends on #14.

`reduce` and family

2

Add `reduce? : C -> (t -> t) -> Option t` with default implementation for any `Fold`able collection

feat: lift StateM to StateT

2

I feel like this might already exist somewhere, but with a not too old Std/Mathlib imported it does not exist yet.

feat: Sum.left, Sum.right

4

More intuitive names than `.inl` and `.inr` for non-type-theorists. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/No.20Either.20type