External/public, better options

doc/spec/02.notation.tex

@@ -0,0 +1,50 @@
+\section{Notation}
+
+Pairs and tuples:
+
+\[
+\inbr{\bullet,\,\bullet,\,\dots}
+\]
+
+Lists of elements of kind $X$:
+
+\[
+X^*
+\]
+
+Deconstructing lists into sublists:
+
+\[
+h\circ t
+\]
+
+This applies also to lists of length 1. Empty list is denoted
+
+\[
+  \epsilon
+\]
+
+
+For a mapping $f : X\to Y$ we use the following definition:
+
+\[
+f [x\gets y] = \lambda\,z\,.\,
+\left\{
+\begin{array}{rcl}
+  y    &,& x = z \\
+  f\;x &,& x\neq z
+\end{array}
+\right.
+\]
+
+Empty mapping (undefined everywhere) is denoted $\Lambda$, the domain of a mapping $f$~--- $\dom{f}$, and we abbreviate
+
+\[
+  \Lambda[x_1\gets y_1][x_2\gets y_2]\dots[x_k\gets y_k]
+\]
+
+as
+
+\[
+  [x_1\gets y_1,\,x_2\gets y_2,\,\dots,\,x_k\gets y_k]
+\]