The Coq mailing list

["Lukasz Stafiniak" <l_stafiniak AT hoga.pl>]

Hi,

How to get the identifier of nth hypothesis, counting from the last one
introduced? I've tried:

Match n With
 [(1)] -> (Match Context With [ id : ?1 |- ? ] -> TacInHyp id ?1)
 | [(2)] -> (Match Context With [ id : ?1; _ : ? |- ? ] -> TacInHyp id ?1)
 | ...

but this doesn't work.

(BTW: can I use "native" integers? I only pass n to the tactic from the
toplevel, I don't compute it.)

Thank You in advance,
Kindest Regards,
Lukasz

PS. The "trick" <Let v = Check t in > was just what I intended. Can any
other commands be used this way?





Uwaga! Do koñca sierpnia przed³u¿yli¶my promocje, do pakietów
wielostanowiskowych dok³adamy PenDrive  Sprawd¼:
http://www.mks.com.pl/promocja-mobile.html