The above comment relates to another error that SANY raises, which I have been considering
opening an issue about. The error has the form:
"Function 'f' is defined with 1 parameters, but is applied to 2 arguments."
when SANY sees `f[a, b]` after a definition of the form `f == [t \in S \X S |-> e(t[1], t[2]) ]`.
I understand the motivation for raising an error in this case, to avoid what will usually indicate
a reasoning error, but based on my understanding of TLA+ this seems valid TLA+ (p.303 in the TLA+ book
and the untyped nature of TLA+). The function application can always be rewritten equivalently
without syntactic sugar as `f[ << a, b >> ]`, thus avoiding the SANY error. So raising this error
does not restrict what one can express.
I am unable to reproduce this issue. For example, SANY accepts
LEMMA
ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
PROVE LET f == [x \in S \X S |-> e(x[1], x[2])]
IN \A x \in S : IsFiniteSet({f[x,y] : y \in S})
Could you please expand?
Thanks,