classical.arbitrary vs nonempty.some

Stream: general

[Eric Rodriguez]

I just noticed that docs#classical.arbitrary exists; I've personally always used docs#nonempty.some. Do people have any preference for which should stay/go? They are syntactically the same thing :) I think nonempty.some is more sensible, as it allows dot notation too; but their (non-dot notation) usages seem to be about the same.

E: one takes instance, one doesn't. don't mind me

[Eric Rodriguez]

/poll What should we do?
Keep nonempty.some
Keep classical.arbitrary
Keep both

[Yaël Dillies]

Given that they are literally defined in the same place, I'd assume people figured both were useful.

[Eric Rodriguez]

feels unmathliblike to do it still...

[Eric Rodriguez]

Ohh, I just noticed; one takes as instance, one doesn't

[Yaël Dillies]

Well, one of them takes the assumption as an instance, the other one does not, and the precise value doesn't matter. So this does look like a technical thing.

[Eric Wieser]

Note that docs#classical.choice has the same signature as nonempty.some, but of course the latter exist for dot notation