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
\documentclass[compress,notes=hide]{beamer}
\let\oldImplies=\implies
\let\implies=\undefined
\usepackage{tlatex}
\begin{document}
\begin{frame}{Slide title}
\begin{tla}
IF pc = "start" THEN
i' \in 0..1000 /\
pc' = "middle"
ELSE IF pc = "middle" THEN
i' = i + 1 /\
pc' = "done"
ELSE FALSE
\end{tla}
\begin{tlatex}
\@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}}%
\end{tlatex}
\end{frame}
\end{document}
Best regards,
Marko
--
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