coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michael Day <mikeday AT yeslogic.com>
- To: Adam Koprowski <adam.koprowski AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Hints and the crush tactic
- Date: Tue, 30 Mar 2010 20:06:55 +1100
Hi Adam,
Note that auto must solve the goal completely or else it will not change the goal in any way. When you apply this tactic directly does it solve the goal completely? Or just "work" giving a new obligation? Can this new obligation be solved by auto?
Right, it isn't sufficient to solve the whole goal, I was just hoping to unpack the hypothesis and subst the equalities with crush and then use other tactics to make further progress.
The crush tactic seems to use autorewrite hints, but I don't see how to trigger this kind of extern hint in this way.
In the meantime, I can always bind it to a new Ltac tactic and call that manually, which would still be shorter than typing out the whole line each time :)
Cheers,
Michael
--
Print XML with Prince!
http://www.princexml.com
- [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Matthieu Sozeau
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
Archive powered by MhonArc 2.6.16.