Stream: math-comp users

Topic: ✔ Converting interval membership into comparisons


view this post on Zulip Yves Bertot (May 02 2023 at 09:30):

Hello, I would like to convert

x \in `]0, 1[

into
0 < x < 1
because the latter can be used by lra. How do I do that?

view this post on Zulip Pierre Roux (May 02 2023 at 09:32):

Does rewrite in_itv works?

view this post on Zulip Kazuhiko Sakaguchi (May 02 2023 at 09:39):

I added it as my TODO on the Algebra Tactics side. It's not clear to me how to do that, but it should be doable. https://github.com/math-comp/algebra-tactics/issues/73

view this post on Zulip Yves Bertot (May 02 2023 at 09:40):

The solution proposed by @Pierre Roux is good, but I am disappointed that search did not help me find it.

view this post on Zulip Notification Bot (May 02 2023 at 09:40):

Yves Bertot has marked this topic as resolved.


Last updated: Jul 23 2024 at 20:01 UTC