Definitions appear one after the other. An ASSUME clause asserts a formula (which may be a conjunction), and it can be named as inASSUME 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.StephanOn 26 Jan 2025, at 22:40, marta zhango <marta...@xxxxxxxxx> wrote:Then, assumptions are just set one after the other?ExampleASSUME 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.StephanOn 25 Jan 2025, at 21:59, marta zhango <marta...@xxxxxxxxx> wrote:I have two elisp exprossions that I want to claim are equivalentTHEOREM 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 /\ notationto 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+u...@xxxxxxxxxxxxxxxx.To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ca79ff6c-9f86-4e5f-90cd-52c55d1f2345n%40googlegroups.com.