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

[Haruki Okada <ocadaruma@xxxxxxxxx>]

[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.