Stream: Coq users

Topic: omega


view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:08):

Unable to locate library Omega. (While searching for a .vos file.)

Did it get renamed?

view this post on Zulip Laurent Théry (Feb 18 2022 at 21:15):

it has been replaced by the lia tactic

Require Import Lia ZArith.

Lemma lem1 :
 forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
Proof.
intros x y.
 lia.
Qed.

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:17):

oof thank you!


Last updated: Feb 08 2023 at 22:03 UTC