Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Instantiations with apply - impossible to unify

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instantiations with apply - impossible to unify


chronological Thread 
  • 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.



Archive powered by MhonArc 2.6.16.

Top of Page