roption mem relation

Stream: general

[Johan Commelin]

@Mario Carneiro You said that the mem relation is better (in the sense of: more idiomatic) than get when working with roption.
Does that mean that you would think it's a good idea of things like enat and multiplicity were refactored to use the mem relation?

[Mario Carneiro]

It depends on what you want to say. enat is a perfectly good totally ordered semiring, and you can use it like that; you can assert that an enat is less/greater than a nat by embedding the nat, and so it's also natural to talk about a finite enat using the standard coercion. This should be proven equivalent to using the mem relation though.

[Mario Carneiro]

I marginally prefer a \in o to o = some a for option and roption

[Mario Carneiro]

it also generalizes nicely to functional relations like the derivative

[Johan Commelin]

What I mean is that currently every other line in those files has get ... in it. I was wondering if we should replace those statements by some ... \in ... statement.

[Mario Carneiro]

You need to use get when making a total function from a partial function that is provably total, but the use should be hidden behind a definition, as we often do with classical.some