\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}