hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
198 stars 40 forks source link

Improvements to Operators and Value chapter #60

Open acud opened 1 year ago

acud commented 1 year ago

Greetings,

I've identified a couple of minor points that can be improved in the aforementioned chapter.

The first is the following paragraph:

There is one more boolean operator of note: =>, or “implication”. A => B means “A is at least as true as B”. A => B = FALSE when false if A is true and B is false, otherwise it’s true. B is true or A is false (or both). You don’t see this very often in programming, as it’s pretty useless for control flow. But it’s extremely important for any kind of specification work. We’ll go into more detail about it later.2

As feedback, I feel that it can be improved in the following manner(s):

In the section of contrapositives exercise:

In the summary section, adding the implication with a very short explainer would be helpful.