coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Michael <michaelschausten AT googlemail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Instantiations with apply - impossible to unify
- Date: Sun, 04 Jul 2010 09:03:20 -0400
Michael wrote:
apply asr_2 with (x:=1000) (y:=1) (z:=4).
Save.
This, however, gives me the error:
Impossible to unify "asr 1000 (1+4) = asr (asr 1000 1) 4" with "1<= asr 10000
5)". How can I apply the Lemmas to solve "test1"?
You probably want [rewrite] instead of [apply], and you might need to [change] the conclusion first so that [rewrite] knows the conclusion matches your lemma. Please see the manual entries on these tactics.
- [Coq-Club] Instantiations with apply - impossible to unify, Michael
- Re: [Coq-Club] Instantiations with apply - impossible to unify, Adam Chlipala
- <Possible follow-ups>
- Re: Re: [Coq-Club] Instantiations with apply - impossible to unify, Michael
Archive powered by MhonArc 2.6.16.