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 12:44:47 +1100
Hi Adam,
Hint Extern 3 =>
match goal with
| H : ?X ++ ?Y = nil |- _ => apply app_eq_nil in H; destruct H; subst
end : cpdt.
That looks perfect! But sadly it doesn't quite seem to work :)
Is the name of the hypothesis significant, or will it match any hypothesis with that form? Is the number 3 important? Is the syntax correct? I've tried adding some fail tactics to debug it, but they never seem to trigger.
Best regards,
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.