Hi ,
I am trying to write the following definition in HOL Light:
let y_5_check4 = define `! (z:real^N)(s:num). y_5_check4 z s =
( transp ( y_5 z s ))$1$1`;;
Given that :
let y_5 = new_definition`!(z:real^N)(s:num) . y_5 z s = lambda i j .
> if ( 1<=i /\ i<=s) then z$i else &0`;;
But it fails with the following exception:
Failure "new_definition: Type variables not reflected in constant".
It is not giving any error when i use same function (y_5) like following:
let y_5_check5 = define `! (z:real^N)(s:num) . y_5_check5 z s = transp (
y_5 z s )`;;
Can someone please explain the error in my first definition?
------------------------------------------------------------------------------
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
