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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Mar 2023 08:35:37 +0200*References*: <CABj=xUVYE8ZRF=8BNj8bDkU9fELtk1UNjVBfDYWC0ebhM8TkFA@mail.gmail.com>

Hi Andrew, TLAPS behaves as expected: all proofs that you wrote are successfully checked by the prover, and they are all valid. However, the level-2 QED step has no proof, and it is therefore not checked. Were you using the Toolbox, you'd see that step (and the assertion of the theorem) colored yellow, indicating that proofs are missing. Should the command-line version display information about missing proofs more prominently by default? Perhaps, but that's not the way it is programmed today, and as you found out, you can obtain that information using the --summary command-line option. 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/BB10F913-6529-4B04-ABC6-B2BE7200445A%40gmail.com. |

**References**:**[tlaplus] Help understanding why this proof validates***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: Help understanding why this proof validates** - Next by Date:
**Re: [tlaplus] Optimizing proof check time** - Previous by thread:
**[tlaplus] Re: Help understanding why this proof validates** - Next by thread:
**[tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Index(es):