Equality of records

Dec 9, 2010 at 2:33 PM

Hi all,

I was playing a bit wit the equality of records, and figured out that it is defined somehow different from a simple equality of all the fields of a record.  So the following example doesn't run through.

#include "vcc.h"

typedef struct vcc(record) A {
  int i;
} A;

void foo()
  assert(forall(A a1; A a2; (a1==a2) <==> (a1.i==a2.i)));

The problem is with the direction from right to left. So from equality of all the fields of a record I can not infer the equality of these records. Is this the intended behavior?

Dec 9, 2010 at 2:38 PM

Ok, I just found that this is done by design (http://vcc.codeplex.com/workitem/3348). Sorry for the inconvenience.