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

Re: Recursive definitions of higher-order operators

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. 


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,