Hi!
I'm new to TLA+, and so far I love it! I've begun using it to specify a distributed data store.
So far I have one small issue (and a few bigger ones, which will require another post): the requirement for all definitions to be defined before their use may impose a less-than-ideal organization on the spec, which might harm its readability. My question is, is it safe/idiomatic to use the RECURSIVE declaration as a forward declaration in the general case (i.e. not for operators that are actually recursive, nor immediately preceding the definition)?
Ron