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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 16 Dec 2020 11:38:55 +0100*References*: <3a468826-b8f0-40af-b8d6-0460adac2b71n@googlegroups.com>

I'm afraid higher-order constant parameters are illegal in TLA+. Section 17.5.2 (p.329) of Specifying Systems saysA declaration statement has one of the forms 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: -- 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. |

**References**:**[tlaplus] How do define a higher-order CONSTANT operator?***From:*Nam Nguyen

- Prev by Date:
**[tlaplus] How do define a higher-order CONSTANT operator?** - Next by Date:
**[tlaplus] formulate property** - Previous by thread:
**[tlaplus] How do define a higher-order CONSTANT operator?** - Next by thread:
**[tlaplus] formulate property** - Index(es):