[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A question

On Mon, Apr 08, 2002 at 04:41:28PM -0400, Da Qi Ren wrote:
> We have a given record data type in PVS, like
> 
> Messages:type=[P:Char, Tm:Clock, Km:Index,No:nat]

The syntax for records is

Messages: type = [# P:Char, Tm:Clock, Km:Index, No:nat #]

You can then access the fields with:

m: Messages  % member of Messages

m`P   m`Tm   etc.

Christoph Berg
-- 
cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
Office +49/681/302-4129, Fax -4290, Home +49/681/9657944
Computer Science Dept., Universität des Saarlandes, Saarbrücken

PGP signature