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

*From*: Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>*Date*: Thu, 3 Nov 2022 01:46:52 -0700 (PDT)

What is the most mathematical way of defining a binary number in TLA+.

My guess is something like the following:

data32 == << b_0 \in {0,1}, ... , b_31 \in {0,1} >>

However, this results in a syntax error.

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/acf45a9b-12cc-4189-8094-750721df34cbn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: Help in evaluating TLA+ as a tool for a CRM application** - Next by Date:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Previous by thread:
**Re: [tlaplus] Meaning of "equivalence" of specifications** - Next by thread:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Index(es):