Re: [tlaplus] Defining multiple expressions and corresponding alignments

Definitions appear one after the other. An ASSUME clause asserts a formula (which may be a conjunction), and it can be named as in

ASSUME A ==

/\ …

A module may contain several ASSUME clauses.

I am not able to read the right-hand sides of your definitions, which are clearly not in TLA+ syntax.

Stephan

On 26 Jan 2025, at 22:40, marta zhango <martazhango@xxxxxxxxx> wrote:

Then, assumptions are just set one after the other?

Example

ASSUME     A1 == (cons extn 'sh-mode)
          A2 == `(,(eval extn) . sh-mode)
                    A3 == extn \in Vars
                       (* extn is a variable that can be evaluated *)
                    A4 == (EX v \in VALUE: ,(eval extn) = v)
                       (* Evaluation of extn results in a value v *)

On Sunday, January 26, 2025 at 7:40:37 PM UTC+12 Stephan Merz wrote:
Definitions are not formulas and can therefore not appear in a conjunction.

Stephan

On 25 Jan 2025, at 21:59, marta zhango <marta...@xxxxxxxxx> wrote:

I have two elisp exprossions that I want to claim are equivalent

THEOREM Expressions E1 and E2 are equivalent (E1 = E2)
ASSUME     E1 == (cons extn 'sh-mode)
       /\ E2 == `(,(eval extn) . sh-mode)

Are the _expression_ names E1 and E1 aligned when using the /\ notation
to define two expressions?

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ed4d67bc-9c98-4d22-b6a2-aef1913c31adn%40googlegroups.com.

--
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 visit https://groups.google.com/d/msgid/tlaplus/ca79ff6c-9f86-4e5f-90cd-52c55d1f2345n%40googlegroups.com.

--
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 visit https://groups.google.com/d/msgid/tlaplus/B766E213-6BEF-4A3A-AC72-A0C24644070F%40gmail.com.