I'm afraid higher-order constant parameters are illegal in TLA+. Section 17.5.2 (p.329) of Specifying Systems says
A declaration statement has one of the forms
CONSTANT c1,...,cn VARIABLE v1,...,vn
where each vi is an identifier and each ci is either an identifier or has the form Op(, ... , ), for some identifier Op.
Perhaps Leslie can shed some light on why that decision was made.
But this only applies to constant parameters, you can of course *define* higher-order operators.
Stephan
On 16 Dec 2020, at 04:35, Nam Nguyen <bitsink@xxxxxxxxx> wrote:
Hi,
I'm trying the following:
``` CONSTANTS X(_, _) LOCAL Err == X(1, LAMBDA y: y) ```
This introduces a parsing error at LAMBDA. If I change X to
CONSTANTS X(_, F(_))
then the parsing error is at F.
How do I define a higher-order constant operator?
Thanks!
-- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3a468826-b8f0-40af-b8d6-0460adac2b71n%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4045C1CC-E452-42BB-B9AD-C437F2063656%40gmail.com.
|