...

[bitonic-mengthesis.git] / final.lagda

diff --git a/final.lagda b/final.lagda
index 8928ec700b5efc0e3c6e20310dbac15d0baed95c..4b7484a9dfb84b161ec3dad25ad9175d05293b69 100644 (file)
--- a/final.lagda
+++ b/final.lagda
@@ -4357,11 +4357,11 @@ Tokenisation is performed by a simple hand written lexer.
     \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
     \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
     \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
-    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
+    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
     \mysee{constrs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
     \multicolumn{3}{@{}l}{\text{Records, and their projections.  The $\mysee{name}$ before the projections is the constructor name.}} \\
-    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
+    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
     \mysee{projs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
   \end{array}