Hi Michael,
Yes, Konrad's right about how types are determined in term quotations,
and I too don't know of an INST in HOL Light that unifies the types of
its arguments.
To get a listing of the types of the free variables in 'th', you can do:
map dest_var (frees th);;
or to return the type of a given variable, where 'x' is the variable
name:
assoc x (map dest_var (frees th));;
Mark.
On 07/01/2018 17:36, Konrad Slind wrote:
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
------------------------------------------------------------------------------
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
