finset.max!

Stream: Is there code for X?

[Adam Topaz]

Do we have an analogue of docs#finset.max which gives a default value for empty finsets? (e.g. if T : finset nat, I it should return 0 for the empty finset).

[Bhavik Mehta]

You can compose the existing one with docs#option.get_or_else, or docs#option.iget

[Adam Topaz]

Thanks!

[Yury G. Kudryashov]

You can also use docs#finset.sup

[Adam Topaz]

Ah, that's probably better suited for my use case! Thanks!