The Coq mailing list

[Florian Haftmann <florian.haftmann AT informatik.tu-muenchen.de>]

Hi Taral,

>>      thus (S q + s = n)
>>        using rewrite n_Sr; simpl; rewrite qsr; reflexivity.
> 
> You probably need to have "by n_Sr, qsr". The using-clause only has
> the minimum number of assumptions available to it.

thanks for the answer.  This doesn't work either.

I was thinking that

>       focus on (S q + s = n). escape.
>         rewrite n_Sr. simpl. rewrite qsr. reflexivity.
>       return. end focus.

and

>       thus (S q + s = n)
>         using rewrite n_Sr; simpl; rewrite qsr; reflexivity.

are equivalent, or at least this is what I thought the documentation says.

It would be helpful to have an explicit hint what is going on here.

Thanks a lot again
        Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature