Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Symmetry does not work with <>

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Symmetry does not work with <>


Chronological Thread 
  • From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Symmetry does not work with <>
  • Date: Mon, 28 Jul 2014 17:10:12 -0300

Hi Guillaume,

That´s not the case, but thanks anyway for sharing your code.

Best Regards,
Marcus.


2014-07-23 9:39 GMT-03:00 gallais <guillaume.allais AT ens-lyon.fr>:
Hi Marcus,

If you use symmetry on inequalities quite a lot in your proof scripts,
you should probably define a wee module making [symmetry] work for [<>].

Here is the way we've done it in Coqtail:
https://github.com/coqtail/coqtail/blob/master/src/mytheories/MyNeq.v

Cheers,
gallais


On 22/07/14 21:46, Marcus Ramos wrote:
​Hi,

My goal is "l <> []"​, however I need it to be "[] <> l". How can I get
this since symmetry does not work for <>?

Thanks,
Marcus.





Archive powered by MHonArc 2.6.18.

Top of Page