X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=notation.tex;h=82a2e647dbac266a769374a422727af8c92e6663;hp=bb12b5ffc5e2faa17090b5b4e6dfe1a9745bb941;hb=bf00a6804e4075d8639f69c96aabf4150506329c;hpb=29344b6ad90d4bc445e67d9b0025509ea555512e diff --git a/notation.tex b/notation.tex index bb12b5f..82a2e64 100644 --- a/notation.tex +++ b/notation.tex @@ -86,15 +86,41 @@ 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: +$C$ has exactly the contents of a git merge result: $\displaystyle 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 + D = C : & \true \\ + D \neq C : & \stmtmergeof{ D \isin L }{ D \isin M }{ D \isin R } \end{cases} $ +We will refer to this as \commitmergename. + \end{basedescript}