an example from the tutorial let th1 = REFL `x+1`;;
val th1 : thm = |- x + 1 = x + 1 # let th3 = INST [`2`,`x:num`] th1;; val th3 : thm = |- 2 + 1 = 2 + 1 Fine. But if we leave off the type information about x it doesn't work. # let th3 = INST [`2`,`x`] th1;; Warning: inventing type variables Exception: Failure "vsubst: Bad substitution list". I don't understand why this fails. In general you might not know what type x has in th1 (eg., has prioritize_real() or prioritize_vector() been done just before this?) . Is there a command I can issue to ask for "the type of `x` in th1 " ? Michael Beeson ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
