+\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+
+\begin{table}
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{term} & ::= & & \mbox{(\bf terms)} \\
+ & & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+ & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+ & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+ & | & \NT{term}~\NT{term} & \mbox{(application)} \\
+ & | & x & \mbox{(identifier)} \\
+ & | & \mathrm{URI} & \mbox{(URI)} \\
+ & | & n & \mbox{(number)} \\
+ & | & \verb+?+ & \mbox{(implicit)} \\
+ & | & \verb+%+ & \mbox{(placeholder)} \\
+ & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+ & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
+ & | & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
+ & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
+ & | & \verb+(+~\NT{term}~\verb+)+ \\
+ & | & \BLOB & \mbox{(blob)} \\
+ \NT{defs} & ::= & & \mbox{(\bf mutual definitions)} \\
+ & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
+ \NT{fun} & ::= & & \mbox{(\bf function)} \\
+ & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
+ \NT{binder} & ::= & & \mbox{(\bf binders)} \\
+ & & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
+ \NT{arg} & ::= & & \mbox{(\bf single argument)} \\
+ & & \verb+_+ \mid x \mid \BLOB \\
+ \NT{ptname} & ::= & & \mbox{(\bf possibly typed name)} \\
+ & & \NT{arg} \\
+ & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
+ \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
+ & & \NT{arg} \\
+ & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
+ \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
+ & & \verb+rec+ \mid \verb+corec+ \\
+ \NT{rule} & ::= & & \mbox{(\bf rules)} \\
+ & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
+
+ \NT{meta} & ::= & & \mbox{(\bf meta)} \\
+ & & \BLOB \\
+ & | & [\verb+term+]~x \\
+ & | & \verb+number+~x \\
+ & | & \verb+ident+~x \\
+ & | & \verb+fresh+~x \\
+ & | & \verb+anonymous+ \\
+ & | & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
+ & | & \verb+default+~\NT{meta}~\NT{meta} \\
+ & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+ & | & \verb+fail+
+\end{array}
+\]
+\end{table}
+