From: Ian Jackson Date: Fri, 16 Mar 2012 23:00:18 +0000 (+0000) Subject: add note about non-exclusivity of \haspatch and \nothaspatch X-Git-Tag: f0.2~5 X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=a8c0dda901340bdd4fb4ca3464f0572c0cab3bd4;hp=26a840c1b223aa5b9d9fd1dc9e7c1922c87cf5f5 add note about non-exclusivity of \haspatch and \nothaspatch --- diff --git a/annotations.tex b/annotations.tex index 26c9bfd..1bf2fcd 100644 --- a/annotations.tex +++ b/annotations.tex @@ -18,8 +18,10 @@ in the summary in the section for that kind of commit. Whether $\baseof{C}$ is required, and if so what the value is, is stated in the proof of Unique Base for each kind of commit. -$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the -set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$ +$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as a +list of $\pq$ for which it is known that $C \haspatch \pq$; +for any $\pq$ not listed, $C \nothaspatch \pq$. +Whether to record $C \haspatch \pq$ in a new commit is in stated (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$ for the ingredients $I$) diff --git a/notation.tex b/notation.tex index 1e19122..2f310bd 100644 --- a/notation.tex +++ b/notation.tex @@ -57,6 +57,8 @@ $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $. $\displaystyle \bigforall_{D \in \py} D \not\isin C $. ~ Informally, $C$ has none of the contents of $\p$. +Note that $\haspatch$ and $\nothaspatch$ are not mutually exclusive. + Commits on Non-Topbloke branches are $\nothaspatch \p$ for all $\p$. This includes commits on plain git branches made by applying a Topbloke patch. If a Topbloke