[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] tlatex fragments and beamer presentations

Dear All,

I'm preparing some beamer slides to summarize some of Leslies video
lectures and it seems there is a conflict between tlatex and
beamer. Apparently \. is defined in both and running latex on the
resulting file will end with

Runaway argument?
! File ended while scanning use of \next.

I intend to use prepare more beamer slides that will involve TLA+ and
would welcome advice on how others deal with this combination.

Here is a simplified example


\begin{frame}{Slide title}
IF pc = "start" THEN 
   i' \in 0..1000 /\
   pc' = "middle"
ELSE IF pc = "middle" THEN
   i' = i + 1 /\
   pc' = "done"
\@x{ {\IF} pc \.{=}\@w{start} \.{\THEN}}%
\@x{\@s{13.31} i \.{'}\@s{5.25} \.{\in} 0 \.{\dotdot} 1000 \.{\land}}%
\@x{\@s{13.31} pc \.{'} \.{=}\@w{middle}}%
\@x{ \.{\ELSE} {\IF} pc \.{=}\@w{middle} \.{\THEN}}%
\@x{\@s{12.29} i \.{'} \.{=} i \.{+} 1 \.{\land}}%
\@x{\@s{12.29} pc \.{'} \.{=}\@w{done}}%
\@x{ \.{\ELSE} {\FALSE}}%

Best regards,


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 on the web visit https://groups.google.com/d/msgid/tlaplus/87h870rhi7.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.

Attachment: signature.asc
Description: PGP signature