max of subsequence

Stream: general

[Andrew Ashworth]

is there a concise way, if I have f : nat -> rat, to obtain the maximum of the sequence as it ranges from 0..N?

[Andrew Ashworth]

i mean, i can definitely apply max recursively N times starting from 0, but then I have to prove a bunch of theorems about the definition

[Mario Carneiro]

Not really. There should be a list.max for this, it seems to come up often. You can at least list.foldl max 0 applied to the list map f (range n)

[Andrew Ashworth]

i will investigate this, thanks

[Mario Carneiro]

I'm not sure that's actually better than just the recursive definition though