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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
