List reduce operation

Stream: lean4

[Alex Sweeney]

I'm still new to Lean and I have a List α that I want to reduce to α using my own function α → α → α. I know in Java it's Stream::reduce:

Optional<T> reduce(BinaryOperator<T> accumulator);

But the documentation for Lean's List is blank (https://lean-lang.org/lean4/doc/list.html). Does something like this already exist in Lean or do I have to make my own? It wouldn't be hard I just don't want to reinvent the wheel

[Damiano Testa]

If you know what you want [] to give, then you can use docs#List.foldl or docs#List.foldr.

[Alex Sweeney]

That's it! Thanks