| Hello, the standard modules are included in the Toolbox distribution, but since you point to a TLAPS directory, you appear to be interested in the proof system. The prover does not use the definitions from the standard modules for reasoning about integers, but encodes TLA+ integers into the corresponding backend theories, for example by injecting the standard sort int of SMT solvers into the universal sort used to represent TLA+ constants. In this way, we can rely on the built-in automation of backends for reasoning about integers. At this point, we do not have any lemmas about ordinary integer reasoning – although it might be useful to state and prove some theorems about non-linear integer arithmetic. However, the directory that you indicate contains the module NaturalsInduction that contains lemmas about inductive reasoning on integers (which backends do not perform automatically), including principles for defining recursive functions over integers. Regards, Stephan
--
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/A96B9E03-9D51-4363-BF26-7E9021760041%40gmail.com. |