RECURSIVE is allowed by the grammar and is handled by TLC. Because of a bug, TLAPS does not handle any spec that uses it. That bug should be fixed before long, but it will be a long time before TLAPS will be able to reason about recursively-defined operators.
On Saturday, October 26, 2013 3:29:13 AM UTC-8, fl wrote:
Hi everybody,A feature that I would appreciate in toobox is the
ability to uncolor and then color everything again
since when we modify a file outside from toolbox
the colors are no longer associated with right lines.
--
FL