Hi,
You can explicitly provide the function type (e.g., y_5:real^N^N) and then
it will work.
Following is a working example:
prioritize_vector();;
let y_y_func = new_definition`
!(z:real^N) (s:num) . (y_y_func:real^N->num->real^N^N) z s = lambda i j.
if ( 1<=i /\ i<=s) then z$i else &0`;;
let main_func = new_definition
`! (z:real^N) (s:num).
main_func z s = (transp (y_y_func z s))$1$1`;;
Thanks
- Umair
On Tue, May 8, 2018 at 10:57 PM, Ayesha Gauhar via hol-info <
hol-info@lists.sourceforge.net> wrote:
> 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
>
>
------------------------------------------------------------------------------
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
