X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=notation.tex;h=48ea1b7e2ceec9002f67b2d41335e5c227b69f25;hp=966c51ec5cd64a6178b9b11bf50b367218ff77db;hb=c497f56e8a7f09c4c328bd7560631d8773b7e676;hpb=891ae7626916bde1eb7dfa38762bbb4d94b85211 diff --git a/notation.tex b/notation.tex index 966c51e..48ea1b7 100644 --- a/notation.tex +++ b/notation.tex @@ -1,4 +1,7 @@ -\section{Notation} +\stdsection{Notation} + +Throughout, any free variables are implicitly universally quantified +at the outermost level. \begin{basedescript}{ \desclabelwidth{5em} @@ -30,8 +33,16 @@ is to be taken as applying to both $\py$ and $\pn$. All of these sets will be disjoint by construction (see Invariants, below). Hence: +\item[ $\foreign$ ] +The set of all commits which are not part of a Topbloke branch. We +call these foreign commits. + +\item[ $\set A$, $\set P$, $\ldots$ ] +Arbitrary sets of commits. Maybe $\set P = \p$ i.e.\ some $\py$ or $\pn$, but +maybe not. + \item[ $\patchof{ C }$ ] -Either $\p$ s.t. $C \in \p$, or $\bot$. +Either $\p$ s.t. $C \in \p$, or $\foreign$. A function from commits to patches' sets $\p$. \item[ $\pancsof{C}{\set P}$ ]