Hi, there:
I'm a new user of hol-light and I find the following thing strange :
# BETA_CONV `(\x. ?y. x = a /\ y = b) y`;;
Warning: inventing type variables
val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b)
the ?y is not renamed in the substitution , is this a bug ?
or am I wrong at some where?
Thanks in advance.
------------------------------------------------------------------------------
Achieve unprecedented app performance and reliability
What every C/C++ and Fortran developer should know.
Learn how Intel has extended the reach of its next-generation tools
to help boost performance applications - inlcuding clusters.
http://p.sf.net/sfu/intel-dev2devmay
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
