diff --git a/tex/iris.sty b/tex/iris.sty index 7d29b29050623c3e325f364ef7df70af0d0fe17d..9dbdc4842415d52eac6fffad1ee03b63e6ffafad 100644 --- a/tex/iris.sty +++ b/tex/iris.sty @@ -332,8 +332,24 @@ %% Hoare Triples -% needs extra {...} for some weird reason -\newcommand{\curlybracket}[1]{{\left\{#1\right\}}} +\newcommand*{\hoaresizebox}[1]{% + \hbox{$\mathsurround=0pt{#1}\mathstrut$}} +\newcommand*{\hoarescalebox}[2]{% + \hbox{\scalerel*[1ex]{#1}{#2}}} +\newcommand{\triple}[5]{% + \setbox0=\hoaresizebox{{#3}{#5}}% + \setbox1=\hoarescalebox{#1}{\copy0}% + \setbox2=\hoarescalebox{#2}{\copy0}% + \copy1{#3}\copy2% + \; #4 \;% + \copy1{#5}\copy2} + +\newcommand{\irisbracketgen}[4][]{% + \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}% + \scalerel*[1ex]{#2}{\copy0}% + {#4}% + \scalerel*[1ex]{#3}{\copy0}} +\newcommand{\curlybracket}[2][]{\irisbracketgen[{#1}]\{\}{#2}} \NewDocumentCommand \hoare {m m m O{}}{ \curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%