From 25fd603a7ef29d937d036ae9abd17548f3ccf5c0 Mon Sep 17 00:00:00 2001
From: Daira Hopwood <daira@jacaranda.org>
Date: Mon, 12 Feb 2018 13:05:23 +0000
Subject: [PATCH] Notation.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
---
 protocol/protocol.tex | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/protocol/protocol.tex b/protocol/protocol.tex
index 813b149d..aea9df42 100644
--- a/protocol/protocol.tex
+++ b/protocol/protocol.tex
@@ -604,6 +604,7 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 \newcommand{\setof}[1]{\{{#1}\}}
 \newcommand{\barerange}[2]{{#1}\,..\,{#2}}
 \newcommand{\range}[2]{\setof{\barerange{#1}{#2}}}
+\newcommand{\rangenozero}[2]{\range{#1}{#2} \difference \setof{0}}
 \newcommand{\alln}{\barerange{1}{n}}
 \newcommand{\minimum}{\mathsf{min}}
 \newcommand{\maximum}{\mathsf{max}}
@@ -623,6 +624,8 @@ electronic commerce and payment, financial privacy, proof of work, zero knowledg
 \newcommand{\leftarrowR}{\buildrel{\scriptstyle\mathrm{R}}\over\leftarrow}
 \newcommand{\union}{\cup}
 \newcommand{\intersection}{\cap}
+\newcommand{\difference}{\setminus}
+\newcommand{\suchthat}{\,\vert\;}
 \newcommand{\lincomb}[1]{(\kern-.025em{#1}\kern-0.04em)}
 \newcommand{\constraint}[3]{\lincomb{#1}\hairspace \times\hairspace \lincomb{#2}\hairspace =\hairspace \lincomb{#3}}
 
@@ -1507,7 +1510,20 @@ $\length(S)$ means the length of (number of elements in) $S$.
 
 $T \subseteq U$ indicates that $T$ is an inclusive subset or subtype of $U$.
 
-$S \union T$ means the type corresponding to the set union of $S$ and $T$.
+\notsprout{
+$\setof{x \typecolon T \suchthat p(x)}$ means the subset of $x$ from $T$
+for which $p(x)$ holds.
+}
+
+$S \union T$ means the set union of $S$ and $T$, or the type corresponding
+to it.
+
+$S \intersection T$ means the set intersection of $S$ and $T$.
+
+\notsprout{
+$S \difference T$ means the set difference obtained by removing elements
+in $T$ from $S$, i.e. $\setof{x \typecolon S \suchthat x \neq T}$.
+}
 
 $\byteseqs$ means the type of bit sequences constrained to be of length
 a multiple of 8 bits.