Something like Haskell's `Foldable`?

Stream: lean4

[Ben Selfridge]

Is there something analogous to Foldable in lean?

[Matt Diamond]

Not sure, but the docs for Mathlib.Control.Fold have some relevant text:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Control/Fold.html

Specifically:

A special class could be defined for foldable, similarly to Haskell, but the author cannot think of instances of foldable that are not also Traversable.

[Matt Diamond]

It looks like foldl/foldr are defined for Traversables in that file

[Ben Selfridge]

Ah! That makes sense. Traversable and Foldable pretty darn close to the same thing.

[Alok Singh]

There was https://github.com/JamesGallicchio/LeanColls/ but it's been a bit since it was updated. I wish this was in batteries, these typeclasses show up a lot