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

Re: [tlaplus] How do define a higher-order CONSTANT operator?



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(page347image50115520, ... , page347image50114176), 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.