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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 30 May 2020 14:32:37 +0200*References*: <f79f5661-f069-4921-9796-420006e2f517@googlegroups.com>

Hello, your syntax for specifying the function is not correct. Instead, try (0 :> 5) @@ (1 :> 8) @@ (2 :> 4) or [x \in 0 .. 2 |-> IF x = 0 THEN 5 ELSE IF x = 1 THEN 8 ELSE 4] If you choose to index your functions from 1, you can simply write <<5 ,8 4>> since a function with domain 1..N is a sequence in TLA+. 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/997736BC-1D57-4044-ABF2-E48921171CE5%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] how to input an array constant in TLA+ toolbox?***From:*biao zhang

**References**:**[tlaplus] how to input an array constant in TLA+ toolbox?***From:*biao zhang

- Prev by Date:
**[tlaplus] how to input an array constant in TLA+ toolbox?** - Next by Date:
**Re: [tlaplus] how to input an array constant in TLA+ toolbox?** - Previous by thread:
**[tlaplus] how to input an array constant in TLA+ toolbox?** - Next by thread:
**Re: [tlaplus] how to input an array constant in TLA+ toolbox?** - Index(es):