Skip to content
This repository has been archived by the owner on Jul 2, 2022. It is now read-only.

Mention that higher-order recursive operators are a bug #98

Closed
zwergziege opened this issue Apr 23, 2021 · 0 comments
Closed

Mention that higher-order recursive operators are a bug #98

zwergziege opened this issue Apr 23, 2021 · 0 comments

Comments

@zwergziege
Copy link

The page on operators contains an example that features a higher-order recursive operator, which is illegal. I know it was deemed more of a happy coincidence and remains untouched for now, but it gets confusing if you write specs like

RECURSIVE Bug(_,_)
Bug(a,b(_)) == 1

which is not covered by the bug and produces an error message, which I in turn thought was a bug until I realized that HOROs are illegal in the first place. Apparently, there's a bug in the bug. To avoid such confusion it would be nice if the page would contain a short note that HOROs are a bug / not actually supported.
Suggestion:

{{% notice note %}} While technically TLA+ does not permit recursive higher-order operators (like the one above) TLC partially supports them due to a bug {{% /notice %}}

I know it was filed by the author of the page, but for the sake of completeness: tlaplus/tlaplus#57

@hwayne hwayne closed this as completed Jul 1, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants