PlusCal expressions are the same as those in TLA+, and if your question is if the formulas in the definitions below:
Reverse(s) == [i \in 1 .. Len(s) |-> s[Len(s)-i+1]
IsMirrorSeq(seq) == \E s \in Seq(Nat) : seq = s \o Reverse(s)
are well-formed TLA+ formulas, the answer is yes.
Tools for TLA+ impose different restrictions on what kind of formulas they can handle. For example, TLC will not be able to evaluate the formula IsMirrorSeq(<<0,1,1,0>>) out of the box, but you can override the Seq operator to impose a bound on the length of sequences. More information on how to do this is available in the Help pages.
Hope this helps,
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/9B4878A6-3141-4D83-AA54-DF2762A26412%40gmail.com.