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

[PVS-Help] Records and quantifying over fields

If I  have a record type (and constants of that type), is it possible to 
quantify over the fields?

World : TYPE = [# p11, p12, p13,
                   p21, p22, p23,
                   p31, p32, p33: Position(3) #]

Given a world, w, I would like to say something like

exists (p,q: positions in w) : p = q

(Actually, what I want to say about p and q is more complicate, but I 
think this is enough to explain my problem).

Is this possible? Or should I be looking at another type (array maybe) 
in the first place?

Dr. Hanne Gottliebsen    Department of Computer Science
hago@dcs.qmul.ac.uk      Queen Mary, University of London
Ph: +44 (0) 207 882 5259
   - I want a single-skin cotton tent like Mr Weasley's