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

The implementation of records and functions in TLC


I would like to know the difference between FcnRcdValue, FcnLambdaValue and RecordValue. 

Moreover, I tried the following code:

TypeOK ==
  /\ FcnSet = [ Int -> Int ]
  /\ RcdSet = [ f1 : Int, f2 : Int ]
and received a TLC error, "Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn], but can't enumerate the value of the `f1' field: Int". I guess TLC tries to enumerate RcdSet. Why does it need to do that? I see that TLC doesn't enumerate FcnSet.

Thanh Hai