blob: 6be0b3d2ba6eee3ebdc4c4ee845bff234a46acde (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
\RequirePackage{amssymb}
\let\eventually\lozenge
\let\always\square
\def\until{\mathop{\mathsf U}}
\def\untilW{\mathop{\mathsf W}}
\let\then\Rightarrow
\def\potentially{\exists\eventually}
\def\inevitably{\forall\eventually}
\def\potentiallyalways{\exists\always}
\def\invariantly{\forall\always}
% The below is taken from the circle package; https://www.ctan.org/pkg/circle
% However, circle is not available in texlive, so this is easier.
\newcommand*\Circle[1][n]{%
\mathchoice{\@Circle{#1}{\tf@size}}{\@Circle{#1}{\tf@size}}%
{\@Circle{#1}{\sf@size}}{\@Circle{#1}{\ssf@size}}%
}
% Bugs: circles have size n at fontsize 2n-1 and 2n; they do not scale linearly
% depending on the fontsize
\newcommand*\@Circle[2]{{%
\dimen0=#2pt \advance\dimen0by4.5pt \dimen1=1pt \divide\dimen0by\dimen1
\count255=\dimen0 \ifodd\count255 \advance\count255by1 \fi\divide\count255by2
\ifnum\count255=0 {}\else\ifnum\count255>15 {}\else
\dimen0=\count255pt
\edef\circfont{tencirc\ifnum\count255>8 w\fi}
\advance\count255by\if #1f111\else 95\fi
\dimen2=.82\dimen0 \advance\dimen2by.4pt
\raisebox{.5\dimen0}[\dimen2]{\makebox[1.2\dimen0]{%
\hspace*{.9\dimen0}%
\csname\circfont\endcsname
\char\count255 %
}}%
\fi\fi
}}
\let\next\Circle
\let\eval\Downarrow
\def\mlif#1#2#3{\mathbf{if}\;#1\;#2\;#3}
\def\mllet#1#2#3{\mathbf{let}\;\mathit{#1}=#2\;\mathbf{in}\;#3}
\def\Bool{\mathbf{Bool}}
|
