From ee8476c4457d9ad51b4995416f1b77a3d4c37e57 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 21 May 2022 11:40:16 +0200
Subject: [PATCH] add short-circuiting boolean operations

---
 tex/heaplang.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 8b895d129..95b1961b5 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -270,6 +270,8 @@ We recover many of the common language operations as syntactic sugar.
   \Let \lvar = \expr in \expr' \eqdef{}& (\Lam \lvar. \expr')(\expr) \\
   \expr; \expr' \eqdef{}& \Let \any = \expr in \expr' \\
   \Skip \eqdef{}& \TT; \TT \\
+  \expr_1 \mathop{\&\&} \expr_2 \eqdef{}& \If \expr_1 then \expr_2 \Else \False \\
+  \expr_1 \mathop{||} \expr_2 \eqdef{}& \If \expr_1 then \True \Else \expr_2 \\
   \Ref(\expr) \eqdef{}& \Alloc(1,\expr) \\
   \CAS(\expr_1, \expr_2, \expr_3) \eqdef{}& \Snd(\CmpXchg(\expr_1, \expr_2, \expr_3)) \\
   \Resolve \expr_1 to \expr_2 \eqdef{}& \ResolveWith \Skip at \expr_1 to \expr_2
-- 
GitLab