---- MODULE Inner ----
CONSTANT C
THEOREM ep == C
====
---- MODULE Test ----
M == INSTANCE Inner WITH C <- TRUE
THEOREM M!ep
====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 HelwerOn 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
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/defbaba5-38df-4e27-826d-0c5a007b3f1dn%40googlegroups.com.