X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=d85a022ff8fb8388f380325f4ffd4ed9e4330d5d;hp=f40f6a2c508b4877d8fe619685ff8f810f20a63a;hb=400772c417bd54383994df5a227df88adc769171;hpb=fc75f297123c083b696f8d5639a4242a12e70f33 diff --git a/article.tex b/article.tex index f40f6a2..d85a022 100644 --- a/article.tex +++ b/article.tex @@ -66,6 +66,9 @@ \newcommand{\gathbegin}{\begin{gather} \tag*{}} \newcommand{\gathnext}{\\ \tag*{}} +\newcommand{\true}{t} +\newcommand{\false}{f} + \begin{document} \section{Notation} @@ -286,7 +289,7 @@ Ancestors of $C$: $ D \le C $. Contents of $C$: -$ D \isin C \equiv \ldots \lor t \text{ so } D \haspatch C $. +$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. \subsubsection{For $A \haspatch P, D \neq C$:} Ancestors: $ D \le C \equiv D \le A $. @@ -313,16 +316,33 @@ $\qed$ If $D = C$, trivial. For $D \neq C$: $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$ -\section{Test more symbols} - -$ C \haspatch \p $ - -$ C \nothaspatch \p $ +\section{Merge} -$ \p \patchisin C $ +Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$): +\gathbegin + C \hasparents \{ L, R \} +\gathnext + \patchof{C} = \patchof{L} +\gathnext + D \isin C \equiv + \begin{cases} + (D \isin L \land D \isin R) \lor D = C : & \true \\ + (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\ + \text{otherwise} : & D \not\isin M + \end{cases} +\end{gather} -$ \p \notpatchisin C $ +\subsection{Conditions} -$ \{ B \} \areparents C $ +\[ \eqn{ Merges Exhaustive }{ + L \in \py => \Bigl[ R \in \py \lor R \in \pn \Bigr] +}\] +\[ \eqn{ Tip Merge }{ + L \in \py \land R \in \py \implies \Bigl[ \text{TBD} \Bigr] +}\] +\[ \eqn{ Base Merge }{ + L \in \py \land R \in \pn \implies \Bigl[ R \ge \baseof{L} \land M = + \baseof{L} \Bigr] +}\] \end{document}