Re: The implementation of records and functions in TLC

[fl <freder...@xxxxxxxxxxx>]

> ... but can't enumerate the value of the `f1' field: Int".

Int is the set of all integers. Since it is infinite and TLC try all cases,
it is too big. In that case you redefine the set in your configuration file: Int <- 1 .. 4 
for instance. (Equivalently you can also look for the form in toolbox that allows
to redefine things.)

--
FL