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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 12 Feb 2021 19:19:52 +0100*References*: <187338c0-d08a-4bab-8b93-12ef87c69709n@googlegroups.com>

Hello, as you observed, nesting sets poses no problem. However, I don't think this is what you really are after. First of all, observe that {0,0,0} = {0}. It seems to me that you intend to associate values with indexes and time stamps. So a cache entry (for a given value) could be modeled as a record CacheEntry == [index : Nat, timestamp : Time] and the cache can be modeled as a function from values to cache entries Cache == [ Value -> CacheEntry ] We can now define the initial condition as cache = [ v \in Value |-> [index |-> 0, timestamp |-> 0] ] and you can write something like cache[v1].index < cache[v2].index for comparing the index values for cache entries for values v1 and v2. Hope this helps, Stephan
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/88CD96D7-A5BF-4E1F-93BA-2A3815E31D73%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Set within a set***From:*Anshu ranjan

**References**:**[tlaplus] Set within a set***From:*Anshu ranjan

- Prev by Date:
**Re: [tlaplus] AND operator** - Next by Date:
**Re: [tlaplus] Set within a set** - Previous by thread:
**[tlaplus] Set within a set** - Next by thread:
**Re: [tlaplus] Set within a set** - Index(es):