Hi Yuhui,

I asked a similar question some years ago here:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2004-September/000235.html
See the replies for an explanation of the issue, in particular Roger's emails.


In your case, you need to specialize the theorem z_id_%bij%_thm before adding/stripping into the assumtions, e.g.
a (strip_asm_tac (z_%forall%_elim %SZT% y %>% z_id_%bij%_thm));

Phil


28/05/15 17:18, YuHui Lin wrote:
Dear all,

I get the following error when I tried to instantiated a forall quantifier in 
an assumption which I inserted using asm_tac.

   Exception Fail * Trying to instantiate type variable 'a, which occurs in 
assumption list [z_∀_elim.6006] * raised

The following dummy example can replay this error

set_goal ([], %SZT% %forall% x : %int%; y : %pset% %int% %=>% x %mem% y %or% x 
%notmem% y %>%);
a  (strip_tac);a  (strip_tac);a  (strip_tac);
a (asm_tac z_id_%bij%_thm);
a (z_spec_nth_asm_tac 1 %SZT% y %>%);


What does this error mean ? Where did I do wrong here ? Thanks in advance.


best,
Yuhui




-----
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com



_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to