[tlaplus] Creating a hash-map in TLA+

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