Re: [tlaplus] Writing "PTL" causes a parser error: "Was expecting "==== or more Module body""

[Stephan Merz]

Does your module include "EXTENDS TLAPS"?

Stephan

On 13 May 2025, at 18:42, Francisco José Letterio <fj.le...@gmail.com> wrote:

Hi all. So I'm following the Proof track from the Hyperbook, but I'm stuck at the very beginning. At the start of page 8 (Section 11) the book claims that "putting PTL in a BY clause causes TLAPS to send the obligation to PTL rather than the default backends"

The problem is that as soon as I write PTL on the file, I get the parser error in the title. Did I miss anything here?

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ae60d433-94c9-4d38-806e-4e49baa846d8n%40googlegroups.com.