Re: [PVS-Help] Error: Expression must be a record type

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Ikram,

The quick answer is that you need to add some parentheses:

akc(xsx, (i:nat)):[nat->nat]= ...

Without them, the typechecker treats xsx and i both as nat - it
only uses variable declarations for identifiers whose type is not
explicitly given.  This is described on page 18 of the language
reference.

Regards,
Sam Owre

Ikram Ullah Lali <ikram_lali@yahoo.com> wrote:

> hi all,
>        I am getting problem in type checking. Problem
> is simple as below:
> 
> i have a record say:
> 
>   	 state: TYPE =[#
> 	   jj:nat,
> 	   ww:nat, 
> 	   dd:nat,
> 	   akc: [nat->nat]
>            #]
>          
> I declare as:
>        xsx :VAR [nat->state]
> Then 
> 
> dd(xs):[nat->nat]=
> 		(LAMBDA (n:nat): xs(n)`dd) % works fine
> 
> akc(xsx, i:nat):[nat->nat]=
> 		(LAMBDA (n:nat):xs(n)`akc(i)) 
> 
> % gives error in akc(....) at xs(n)`akc(i) that
> 
> " Expression must be a record type "
> 
> Thanks,
> 
> Ikram
> 
> 
> 
> 
> 
>        
> ____________________________________________________________________________________
> Be a better Globetrotter. Get better travel answers from someone who knows. Yahoo! Answers - Check it out.
> http://answers.yahoo.com/dir/?link=list&sid=396545469