Zulip Chat Archive

Stream: general

Topic: roption mem relation


Johan Commelin (Jun 06 2019 at 00:04):

@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 (Jun 06 2019 at 00:08):

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 (Jun 06 2019 at 00:09):

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

Mario Carneiro (Jun 06 2019 at 00:10):

it also generalizes nicely to functional relations like the derivative

Johan Commelin (Jun 06 2019 at 00:42):

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 (Jun 06 2019 at 01:13):

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


Last updated: Dec 20 2023 at 11:08 UTC