Re: [tlaplus] Defining multiple expressions and corresponding alignments

Definitions are not formulas and can therefore not appear in a conjunction.

Stephan

On 25 Jan 2025, at 21:59, marta zhango <martazhango@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+unsubscribe@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/E594A29B-CC91-43A8-A973-140A772DE27A%40gmail.com.