Question about : symbol in subexpressions of recursive operators

[Andrew Helwer]

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