chiark / gitweb /
notation: define \stmtmergeof and \setmergeof
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 16:23:02 +0000 (17:23 +0100)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 16:23:02 +0000 (17:23 +0100)
article.tex
notation.tex

index 12d7bbc..7bff692 100644 (file)
 \newcommand{\alg}[1]{\text{\bf #1}}
 \newcommand{\setmerge}{\alg{merge}}
 \newcommand{\setmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
+\newcommand{\stmtmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
 
 %\newcommand{\setmergeof}[3]{\setmerge\left\lgroup #1 \;\middle\lmoustache\; #2 \;\middle\rmoustache\; #3 \right\rgroup}
 %\newcommand{\setmergeof}[3]{\setmerge\left\rmoustache #1 \middle\rmoustache #2 \middle\lmoustache #3 \right\lmoustache}
index bb12b5f..b5e0e9d 100644 (file)
@@ -86,6 +86,32 @@ the relevant Topbloke branches, we hope that
 if the user still cares about the Topbloke patch,
 git's merge algorithm will DTRT when trying to re-apply the changes.
 
+\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ]
+The proper results of a merge.  Formally,
+where $L$, $M$ and $R$ are statements:
+
+$$
+  \stmtmergeof{L}{M}{R}
+    \equiv
+  \begin{cases}
+         (L \land R)      : & \true \\
+    (\neg L \land \neg R) : & \false \\
+    \text{otherwise} : & \neg M
+  \end{cases}
+$$
+
+May also be used where $L$, $M$ and $R$ are sets, in which case
+$$
+  \setmergeof{L}{M}{R}
+     =
+  \left\{
+    \;
+    D \; \middle| \;
+      \setmergeof{ D \in L }{ D \in M }{ D \in R }
+    \;
+  \right\}
+$$
+
 \item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
 The contents of a git merge result: