On 13 May 2011, at 08:11, hao deng wrote: > 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? >
It isn't a bug and you aren't doing anything wrong. The variables x and y in your lambda-term will have been assigned different types. In the HOL logic two variables with the same name but different types are distinct. The result of the beta conversion contains two distinct variables both named "y". Unfortunately, the pretty-printer isn't showing you the distinction. Ideally it would have printed something like "?y: 'b.(y: 'a) = a /\ (y: 'b) = b". Regards, Rob. ------------------------------------------------------------------------------ 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
