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:
Just wanted to ask if there are plans to support recursive definitions of higher-order operators in the future?
Thank you,
Yuri