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

Re: The implementation of records and functions in TLC

It is impossible to say exactly what TLC is doing without knowing what the values of FcnSet and RcdSet are.

On Thursday, November 19, 2015 at 2:20:09 AM UTC-8, Hai Tran Thanh wrote:

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