[tlaplus] Re: In SANY, what is the APSubstInNode AST node used for?

I think a broader case is an instantiated theorem with a plain _expression_ body, like the above. That still produces APSubstInNode, even though the theorem body is not ASSUME/PROVE.

On Friday, March 13, 2026 at 4:49:49 PM UTC+1 Andrew Helwer wrote:

I figured this out. The clue was from the SubstInNode, which SANY uses to wrap expressions from modules imported using INSTANCE/WITH with substitutions, so the substitutions are lazily applied instead of directly written. As the name suggests then, APSubstInNode is when the same thing happens to an ASSUME/PROVE block. I don't know why the substitution isn't just distributed over ASSUME/PROVE to affect the expressions within, but whatever; this spec will produce an XML export containing an APSubstInNode instance at the M!ap usage point:

---- MODULE Test ----
---- MODULE Inner ----
CONSTANT C
THEOREM ap == ASSUME C PROVE C
====
M == INSTANCE Inner WITH C <- TRUE
THEOREM M!ap
====

This does not appear in the tlaplus/examples, nor any other TLA+ spec floating around that I can find, so it's a pretty obscure feature that is essentially never exercised. Possibly some bugs lurking within.

Andrew Helwer

On Tue, Mar 10, 2026 at 1:54 PM Andrew Helwer <andrew...@xxxxxxxxx> wrote:
Here is the Java class in question, which is mirrored in the XML export format. I have run the exporter over every spec I can find and as far as I can tell, APSubstInNode is not used in any of them. Is this a zombie language feature or just an obscure one?

Andrew