coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] equality graph
- Date: Wed, 25 Sep 2013 19:43:22 -0400
Hi,
Often I have to prove an equality that can be proven by merely applying transitivity and symmetry on other equalities of the same type in my hypotheses.
I think someone must have already written a tactic which builds an undirected graph of equalities(hypotheses) of the same type and then finds whether a path exists, and build its proof object.
If not, any ideas on the easiest way to achieve this would be appreciated.
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/
- [Coq-Club] equality graph, Abhishek Anand, 09/26/2013
- Re: [Coq-Club] equality graph, Daniel Schepler, 09/26/2013
- Re: [Coq-Club] equality graph, t x, 09/26/2013
Archive powered by MHonArc 2.6.18.