Zulip Chat Archive

Stream: general

Topic: max of subsequence


view this post on Zulip Andrew Ashworth (Feb 27 2018 at 00:06):

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

view this post on Zulip Andrew Ashworth (Feb 27 2018 at 00:10):

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

view this post on Zulip Mario Carneiro (Feb 27 2018 at 00:14):

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)

view this post on Zulip Andrew Ashworth (Feb 27 2018 at 00:14):

i will investigate this, thanks

view this post on Zulip Mario Carneiro (Feb 27 2018 at 00:15):

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


Last updated: May 12 2021 at 05:19 UTC