quint icon indicating copy to clipboard operation
quint copied to clipboard

Published 20 hours ago • verified publisher icon informalsystems

Implement `chooseSome`

Open konnov opened this issue 2 years ago • 0 comments

This is the CHOOSE x \in S: TRUE of TLA+. Most likely, it requires the canonical form, similar to what we do in the conversion toQuintEx. This operator is not a priority.

konnov avatar Jul 21 '22 19:07 konnov