Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Facts about Ensembles

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Facts about Ensembles


Chronological Thread 
  • From: Daniil Frumin <difrumin AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Facts about Ensembles
  • Date: Wed, 9 Jul 2014 15:11:33 +0200

Hi, all

I was just curious about lack of facts for the Ensembles:
http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html

Surely, there are a lot of small (but useful) theorems to state about sets.

Another thing I was actually wondering about, is the possibility of
having rewrites using the Same_set as justifications.
I mean going from

Г, Same_set A B, In A x |- _

to

Г, Same_set A B, In B x |- _


I am not very familiar with Ltac to write it myself, but it does make
sense to me.

Cheers

-- Daniil



Archive powered by MHonArc 2.6.18.

Top of Page