coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Amin Timany, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Guillaume Melquiond, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Robbert Krebbers, 07/09/2014
- Re: [Coq-Club] Facts about Ensembles, Daniil Frumin, 07/10/2014
Archive powered by MHonArc 2.6.18.