How do define a higher-order CONSTANT operator?

[Nam Nguyen]

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!

[Stephan Merz]

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

-- 
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3a468826-b8f0-40af-b8d6-0460adac2b71n%40googlegroups.com.