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

[Ikram Ullah Lali <ikram_lali@xxxxxxxxx>]

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