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

Re: [tlaplus] Creating a hash-map in TLA+



[x \in {key} |-> val]

should work

2022年11月26日(土) 5:23 Aman Shaikh <amanshaikh75@xxxxxxxxx>:
Hi

I'd like to create a hash in TLA+ that maps a key to its value where ..

key == expr1
val == expr2

Doing [key |-> val] creates a record with the field 'key'. What I want is [expr1 |-> expr2]. How do I achieve this?

thx
aman

 

--
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/41e9a4b7-14a9-4e55-bce5-ba54b46b1a38n%40googlegroups.com.


--
========================
Okada Haruki
ocadaruma@xxxxxxxxx
========================

--
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/CAHf4GKqRpmnHvqpr2Hf6Zduszgte8G02oNXBcFLSA8US42rXPg%40mail.gmail.com.