Re: [tlaplus] Defining multiple expressions and corresponding alignments

[marta zhango <martazhango@xxxxxxxxx>]

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.