Hi Michael, What I think is happening is that each quoted element is being parsed separately. This means that the type of the x in `x` is a type variable while the type of `2` is :num. Since INST (I think) just fails if the two types aren't identical, you get the displayed behaviour. There may well be a version of INST in Hol Light that normalizes the arguments but I don't know it.
Konrad. On Thu, Jan 4, 2018 at 8:04 PM, Michael Beeson <profbee...@gmail.com> wrote: > 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 ------------------------------------------------------------------------------ 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
