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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 6 Dec 2015 08:41:29 -0800 (PST)*References*: <75f4c1c5-52ee-4f44-a2fa-8dbadc6599ec@googlegroups.com>

There is no plan to allow recursive definitions of higher-order operators. I believe that Georges Gonthier believes that allowing them is not a problem. I think that supporting them would just require a simple change to the parser and no change to TLC, though I'm not positive about that. However, I found it hard enough to understand the meaning of a recursive definition of an ordinary operator, and I was not able to understand recursive definitions of higher-order operators well enough to be convinced of their soundness. And recursive definitions of first-order operators are still not supported by TLAPS.

Leslie

On Sunday, December 6, 2015 at 7:34:46 AM UTC-8, Y2i wrote:

On Sunday, December 6, 2015 at 7:34:46 AM UTC-8, Y2i wrote:

Just wanted to ask if there are plans to support recursive definitions of higher-order operators in the future?Thank you,Yuri

**References**:

- Prev by Date:
**Recursive definitions of higher-order operators** - Next by Date:
**Re: How to check if a variable increases or stays the same at each new state?** - Previous by thread:
**Recursive definitions of higher-order operators** - Next by thread:
**Re: Recursive definitions of higher-order operators** - Index(es):