From 5a0f0a4c3580b5ce39dfe036965fc04b52f9a005 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Fri, 13 May 2022 16:53:51 +0200
Subject: [PATCH] Made hoare triple macro compatible with e.g. array
 environment

---
 tex/iris.sty | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/tex/iris.sty b/tex/iris.sty
index 7d29b2905..7490f6ea2 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -332,8 +332,25 @@
 
 %% 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{\bracket}[4][]{%
+  \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
+  \scalerel*[1ex]{#2}{\copy0}%
+  {#4}%
+  \scalerel*[1ex]{#3}{\copy0}}
+\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
+\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
 
 \NewDocumentCommand \hoare {m m m O{}}{
 	\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
-- 
GitLab