TLA+ | The way to specify

The RECURSIVE declaration states that depthFirst is an operator that takes two arguments, each of which is a value. The left-hand side of the definition of depthFirst states that it is an operator that takes two arguments, the first of which is a value and the second of which is an operator that takes one argument. Thus, the RECURSIVE declaration and the definition are inconsistent.

A RECURSIVE declaration that is consistent with the definition would have to be something like

RECURSIVE depthFirst(_, _(_))

However, if you try it you will discover that the parser does not accept this declaration. That is not an oversight. TLA+ does not allow recursive definitions of "higher-order" operators--ones that take operators as arguments. The semantics of recursive definitions is quite subtle. It has to give a meaning to something like

RECURSIVE Op(_)
Op(x) == CHOOSE y : y # Op(x)

without introducing inconsistency. I don't know how to do that for recursive definitions of higher-order operators.

Note that there is no problem writing recursive definitions of functions or operators that take functions as arguments. I have found that recursive operator definitions are a convenience, not a necessity, and that it is always possible (though sometimes a lot of trouble) to use recursive function definitions instead. I suggest that you change your definition of depthFirst so it expects a function rather than an operator as its second argument. If you don't know how to make that work, please post an explanation of what you are trying to define and I will try to help you.

Leslie Lamport