The implementation of records and functions in TLC

[Hai Tran Thanh <thanhh...@xxxxxxxxx>]

Hello,

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.

Thanks,

Thanh Hai