Yves Bertot (May 02 2023 at 09:30): 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?
Pierre Roux (May 02 2023 at 09:32):Does rewrite in_itv works?
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
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.
Notification Bot (May 02 2023 at 09:40):Yves Bertot has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC