Skip to content
Snippets Groups Projects
Commit bfb57e8b authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'iris_style_improvements' into 'master'

Make Hoare triple tex macro compatible with e.g. array environment

See merge request iris/iris!797
parents 56e9d264 c4857c8a
No related branches found
No related tags found
No related merge requests found
......@@ -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}%
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment