[tlaplus] Question about : symbol in subexpressions of recursive operators

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Trying to wrap my head around how exactly this subexpression works. From page 14 of the TLA+ 2 language guide we have:

We usually don’t need to name the entire _expression_ to the right of a == because the operator being defined names it. However, as observed in Section 2, this is not true for recursively defined operators. If Op is recursively defined by Op(p1, ..., pk) == exp then Op(P1, ..., Pk)!: names exp with Pi substituted for pi , for each i
in 1 . . k.

Perhaps this is just a case of TLC semantics not matching TLA+ semantics, but I can't seem to find the use of : when referring to a recursive operator like:

RECURSIVE Factorial(_)
Factorial(n) == IF n = 0 THEN 1 ELSE n * Factorial(n - 1)

If I plug in Factorial(3)!3 to the TLC constant _expression_ evaluator, it gives me 6 as you'd expect. If I plug in Factorial(3)!:!3, I get the error:

!: can be used only after a name and either at the end after an operator name or before an operator name.

So what sort of otherwise-inaccessible subexpressions can I address with the : symbol? Thanks!

Andrew

-- 
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/2a659530-59ad-4451-bb20-c2bde444083en%40googlegroups.com.