[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Tue, 11 May 2021 06:49:04 -0700 (PDT)*Ironport-hdrordr*: A9a23:KiY5jKCNBzL78C/lHej8sceALOsnbusQ8zAXPhhKOGFomszxrbHNoByCvSWE+wr5K0tQ5exoX5PwM080lKQFkbX5Uo3SJTUO1FHJEGgm1/qZ/9SCIVyKygc+79YZT0EWMrSZZzcVsS+52njCLz9K+qjjzEncv5a5854bd3APV0gP1XYbNu7qeHcceOFpb6BJc6Z10qB81nCdkQp8VLXOOpEiMtKz0eEi5/jdDCIuNloN4BKUhTm15ba/KDO8mioETylTzbpn3m7fjQTj66m52svWqyM1oAXont9rcKqN8KoNOCQP4PJlZwkFCWyTFchcs8zphkFDnAncgmxa2eUk6C1QQPibo0mhAF1dfiGdkzUI/gxemkPf9Q==

Trying to wrap my head around how exactly this subexpression works. From page 14 of the TLA+ 2 language guide we have:

in 1 . . k.

Perhaps this is just a case of TLC semantics not matching TLA+ semantics, but I can't seem to find the use of : when referring to a recursive operator like:

RECURSIVE Factorial(_)

Factorial(n) == IF n = 0 THEN 1 ELSE n * Factorial(n - 1)

Factorial(n) == IF n = 0 THEN 1 ELSE n * Factorial(n - 1)

If I plug in Factorial(3)!3 to the TLC constant _expression_ evaluator, it gives me 6 as you'd expect. If I plug in Factorial(3)!:!3, I get the error:

!: can be used only after a name and either at the end after an operator name or before an operator name.

So what sort of otherwise-inaccessible subexpressions can I address with the : symbol? Thanks!

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 on the web visit https://groups.google.com/d/msgid/tlaplus/2a659530-59ad-4451-bb20-c2bde444083en%40googlegroups.com.

- Prev by Date:
**Re: [tlaplus] Help：TLA+ Latex symbol table** - Next by Date:
**[tlaplus] How to write my operator which can be used in TLA+** - Previous by thread:
**Re: [tlaplus] Help：TLA+ Latex symbol table** - Next by thread:
**[tlaplus] How to write my operator which can be used in TLA+** - Index(es):