[tlaplus] Describing unless condition in lisp

[marta zhango <martazhango@xxxxxxxxx>]

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)

-- 
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/c929677a-a59c-475c-a753-9090dabd6803n%40googlegroups.com.