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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 10 Nov 2014 11:23:50 -0800 (PST)*References*: <27780607-9e0a-4101-92fa-ccbb15043611@googlegroups.com>

One comment about the hyperbook in particular, the text
description building up proofs is good to follow along and

force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

Agreed.

In general, I have tried to present a complete module after developing it bit by bit. However, sometimes a module isn't developed bit by bit, but a first version is developed, then it is modified to form another version, then modified again and again. So, instead of having a single complete module, there are quite a few. In those cases, it seems impractical to provide a complete module for each of those versions. Perhaps someone has a suggestion on what to do in that case. However, it is possible that there are places where it would be reasonable to provide a complete module (or perhaps a complete proof) and I have failed to do so. I would appreciate having those exact places pointed out.

Thanks,

Leslie

**Follow-Ups**:**Re: Proofs of integer properties***From:*chris . . .

**References**:**Proofs of integer properties***From:*chris . . .

- Prev by Date:
**Re: Proofs of integer properties** - Next by Date:
**Re: [tlaplus] Re: Proofs of integer properties** - Previous by thread:
**Re: [tlaplus] Re: Proofs of integer properties** - Next by thread:
**Re: Proofs of integer properties** - Index(es):