Difficulty completing Reverse(Twople) exercise

[raoulmillais]

Working through the examples one by one, I found I couldn't complete the Twople exercise. I came across 2 problems:

1. I had to peek at the answer of how to reverse a two tuple. I did not know how to raise an error at this point in TLA+, so maybe you should consider introducing this earlier on?

2. The supplied solution didn't work for me when I pasted it into the toolbox (I may be doing something wrong here).

Spec

---------------------------- MODULE LearnTlaPlus ----------------------------
EXTENDS Integers, Sequences
                      
Reverse(Twople) == IF Len(Twople) = 2 THEN <<Twople[2], Twople[1]>> ELSE ASSERT FALSE
               
=============================================================================

Error (truncated for brevity as it's impossible to copy/paste the parse errors on OSX)

***Parse Error***
Was expecting  "==== or more Module body"
Encountered FALSE at ...

[hwayne]

Did I write ASSERT FALSE? Because that's not a real thing. *Headdesk* Sorry about that. I'll change the exercise to "if there's two, reverse, otherwise return original sequence", which should cover both issues.

…

On Sun, Oct 22, 2017, 11:31 AM Raoul Millais ***@***.***> wrote: Working through the examples one by one, I found I couldn't complete the Twople exercise. I came across 2 problems: 1. I had to peek at the answer reverse a two tuple without peeking at the answer. I did not know how to raise an error at this point in TLA+, so maybe you should consider introducing this earlier on. 2. The supplied solution didn't work for me when I pasted it into the toolbox (I may be doing something wrong here). *Spec* ---------------------------- MODULE LearnTlaPlus ---------------------------- EXTENDS Integers, Sequences Reverse(Twople) == IF Len(Twople) = 2 THEN <<Twople[2], Twople[1]>> ELSE ASSERT FALSE ============================================================================= *Error* (truncated for brevity as it's impossible to copy/paste the parse errors on OSX) ***Parse Error*** Was expecting "==== or more Module body" Encountered FALSE at ... — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#38>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACiXdOmPzf6XH04HReYSnNoxnwBxGBUKks5su238gaJpZM4QCAvu> .

[hwayne]

Fixed in 31b6232.

[raoulmillais]

All working for me now when I run it. Thank you very much for your work making this, it's really helpful having plenty of sources to learn from :)