Dear Mr. Sawasta Paul,
You have made a remarkably astute observation. In retrospect, I'm
astonished that no one has noticed this before. The rule that a
symbol can be used only after it is declared or defined makes no
sense, since it makes it impossible to declare or define any symbol.
For example, that rule forbids writing
n == 15
because n isn't defined until after that statement, so it would not be
allowed to appear in that statement. One might attempt to correct the
rule to say that a symbol may appear only in or after its declaration
or definition. However, that would forbid this _expression_
{n+1 : n \in Nat}
(which equals the set of positive integers) because "n+1" comes before
"n \in Nat", which locally declares n.
The precise statement of the rule is that a symbol that is not a built-in
TLA+ symbol can appear only in its declaration or within the scope of
its declaration. This assumes that
RECURSIVE F(_)
is considered to be the declaration of F, and any rule about not defining
a symbol that's already declared must be appropriately weakened to allow
recursive operator definitions.
This demonstrates the difficulty of making correct statements in an
informal language like English. Thank you for pointing it out.
Leslie