X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=final.lagda;h=4b7484a9dfb84b161ec3dad25ad9175d05293b69;hb=df78daffd508f40f39777d37db16562007b2ed12;hp=8928ec700b5efc0e3c6e20310dbac15d0baed95c;hpb=e319c3d9b3de84af2608cfbee8a3a7cbdba19615;p=bitonic-mengthesis.git

diff --git a/final.lagda b/final.lagda
index 8928ec7..4b7484a 100644
--- 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}