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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 30 May 2020 15:48:46 +0200*References*: <f79f5661-f069-4921-9796-420006e2f517@googlegroups.com> <997736BC-1D57-4044-ABF2-E48921171CE5@gmail.com> <779f2d1e-d4f6-49ea-86cd-5dd12922f5b1@googlegroups.com>

Again, if you use sequences (i.e., index from 1), you can just write Len(nums). For your setup, you can define len == 1 + (CHOOSE i \in DOMAIN nums : \A j \in DOMAIN nums : j <= i) 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/3DFE0683-2C25-4170-8B47-AFF7BAE8A2D9%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

**Re: [tlaplus] how to input an array constant in TLA+ toolbox?***From:*Stephan Merz

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

- Prev by Date:
**Re: [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:
**Re: [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):