Describing unless condition in lisp

[marta zhango]

I have the following lisp code, which I want to describe in TLA.

(unless (and actm (not (eq actm 'go)))
    ;;  Insert M newlines after label (default 0).
    ;;  The first newline ends the label line itself
    (dotimes (_ (1+ (or m 0))) (insert "\n"))) )

Came up with this but still now to this and unsure about correctness

(unless COND &rest BODY) If COND yields nil, do BODY.

  LET: \not actm \imlp actm unspecified or nil

           \knj means conjunction

           \dsj  means disjunction

  ACTION: \knj \not COND

          \knj \not (actm \knj \not (actm = 'go))
          \knj \not actm \dsj actm = 'go
          \knj actm = (unspecified, 'go)
 

[Andrew Helwer]

Hi Marta,

If you'd like, we can set up a video call to chat about your interest in TLA+ and what sort of problems you are looking to solve with it! You can reply directly to this message (not to the wider group) to set something up.

Andrew Helwer

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c929677a-a59c-475c-a753-9090dabd6803n%40googlegroups.com.