| Hello Mamoun, just to clarify the context of your question: you refer to the TLA+ Proof System: TLC and Apalache implicitly use all definitions of imported modules). Currently TLAPS does not allow you to make all facts or definitions of a module usable. (This possibility is explicitly mentioned in [1], pp. 20-21, and it is mentioned that the corresponding construct is not implemented in TLAPS and is "likely to be removed from the language".) The rationale is that (1) adding too many facts or definitions may overwhelm backend provers and (2) a change to a module could then easily break proofs in modules that import or instantiate the module, resulting in a maintenance nightmare. Personally, I believe that module writers should be given the possibility to selectively annotate definitions or facts with attributes that could indicate how backend provers could make use of them without manual expansion, similar to the [simp], [intro] etc. attributes that exist in the Isabelle proof assistant. (But the designers of Isabelle then also found that they needed corresponding attributes such as [simp del], resulting in some quite brittle proofs, so there is no silver bullet.) In the meantime, you can insert a directive such as USE foo, bar DEF baz in a module to make selected facts or definitions usable for the remainder of the module. Hope this helps, 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 visit https://groups.google.com/d/msgid/tlaplus/207CB171-FFC6-479E-89D9-1CD9C3462AB7%40gmail.com. |