Re: [tlaplus] Best practice when building a series of model refinements?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 27.02.20 18:55, Shiyao MA wrote:
> Could you post the source of the set, arrayset, and hashset.
> 
> Refinement is relatively opaque to me.  I'd like to know what role
> "refinement" plays here.


See video lecture 10. of Lamport's video course:
https://lamport.azurewebsites.net/video/videos.html

The Set specs are incomplete examples that shouldn't be shared.

Markus

-- 
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/0d38911c-d9e6-61a3-abfd-165e0b66eb3c%40lemmster.de.