search

tlaplus / rfcs

RFCs for changes to the TLA+ specification language
MIT License
13 stars 0 forks source link

Proposal: add `RANGE` prefix operator with built-in implementation #13

Closed ahelwer closed 2 weeks ago

ahelwer commented 2 months ago

This would be defined as:

RANGE f == {f[e] : e \in DOMAIN f}

We have a DOMAIN prefix operator, which I use often, and it would be nice to have a RANGE prefix operator as well. I often end up defining this operator anyway. Precedence would be the same as the DOMAIN operator.

lemmy commented 2 months ago

The Functions module in TLAPS and the CommunityModules comes with a Range operator:

https://github.com/tlaplus/CommunityModules/blob/9c13c116cbcb4975c7d33ee7a71ba471b88687b2/modules/Functions.tla#L65-L70

ahelwer commented 2 weeks ago

Probably a bad idea since there is some confusion of the concept of range with codomain and such. Better to let people define this for themselves.