I got the error:
Error: The reference lia was not found in the current environment.
how do I fix it?
code:
Require Import Lia.
Theorem t:
forall n: nat, 1 + n > n.
Proof.
Show Proof.
intro.
Show Proof.
lia.
Show Proof.
Qed.
I got the error:
Error: The reference lia was not found in the current environment.
how do I fix it?
code:
Require Import Lia.
Theorem t:
forall n: nat, 1 + n > n.
Proof.
Show Proof.
intro.
Show Proof.
lia.
Show Proof.
Qed.
Do Require Import Lia.
at the top. e.g.
Require Import Lia.
Theorem t:
forall n: nat, 1 + n > n.
Proof.
Show Proof.
intro.
Show Proof.
lia.
Show Proof.
Qed.
note this is a replacement for Omega
As Ana Borges kindly pointed out:
Note that according to the Coq changelog, omega was only deprecated in Coq 8.12 and removed in 8.14. If you are using an older version of Coq, you can still make use of it. However, even in 8.11 the recommendation was to switch to lia, and unless you have a very good reason I would recommend updating your Coq installation anyway (the latest is 8.15.2).
coqc --version
on a terminal.8.11.0
@AnaBorgesRequire Import Lia
was not working for you for some reason.omega
was only deprecated in Coq 8.12 and removed in 8.14. If you are using an older version of Coq, you can still make use of it. However, even in 8.11 the recommendation was to switch tolia
, and unless you have a very good reason I would recommend updating your Coq installation anyway (the latest is 8.15.2).