The Coq mailing list

[Vincent <vincent.siles AT gmail.com>]

I'll definitely try lia ! I tried with the Require Import but got an error. Maybe it was disable for this particular (very simple) exercise. Will try again :)

Le ven. 28 juin 2019 à 10:57, Théo Zimmermann <theo.zimmi AT gmail.com> a écrit :

Hi Vincent,

"omega" is available actually: you just need to import it "Require
Import Omega."
Most people nowadays use "lia" though since "omega" is about to be
deprecated in favor of "lia". (Using "lia" requires you to "Require
Import Lia.")

Théo

Le ven. 28 juin 2019 à 10:47, Vincent Siles
<vincent.siles AT ens-lyon.org> a écrit :
>
> I played a bit with it this morning, it's nice. I have the same remark as Agnishom plus a minor one: could Omega be available ? That would be helpful to discharge some annoying arithmetic proofs :D
>
> Le ven. 28 juin 2019 à 10:30, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> a écrit :
>>
>> This is great. Somewhat similar to Proof Ground and Proving for Fun.
>>
>> It is actually quiet difficult to work with the web interface since it does not provide the interactive Coq environment. So maybe we can have a Coq IDE or links for downloading the ``Preloaded" files?
>>
>> --Agnishom
>>
>> On Fri, Jun 28, 2019 at 7:13 AM Donald Leung <i.donaldl AT me.com> wrote:
>>>
>>> I hereby write to you to invite you to sign up for an account on Codewars: https://www.codewars.com
>>>
>>> Codewars is a training platform where programmers of all disciplines train on code challenges called Kata in order to improve their programming skills. The Coq proof assistant was recently added to Codewars (approx. April 2019) and there are currently insufficient Coq users to push newly authored Coq challenges out of the Beta (testing) phase; therefore, it would be an honor to have a seasoned Coq user like you on Codewars to test them out and contribute more interesting Coq challenges to the community.
>>>
>>> Should you choose to create an account on Codewars, you are also welcome to ask any questions about the Codewars platform in general or simply chat with other Codewarriors via our Gitter channel: https://gitter.im/Codewars/codewars.com
>>>
>>> Yours sincerely,
>>> Donald Sebastian Leung
>>> A Year 2 CSE undergraduate at The Hong Kong University of Science and Technology