equal
deleted
inserted
replaced
57 \subcaption{Binders} |
57 \subcaption{Binders} |
58 |
58 |
59 \begin{center} |
59 \begin{center} |
60 \index{*"= symbol} |
60 \index{*"= symbol} |
61 \index{&@{\tt\&} symbol} |
61 \index{&@{\tt\&} symbol} |
62 \index{*"| symbol} |
62 \index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working |
63 \index{*"-"-"> symbol} |
63 \index{*"-"-"> symbol} |
64 \index{*"<"-"> symbol} |
64 \index{*"<"-"> symbol} |
65 \begin{tabular}{rrrr} |
65 \begin{tabular}{rrrr} |
66 \it symbol & \it meta-type & \it priority & \it description \\ |
66 \it symbol & \it meta-type & \it priority & \it description \\ |
67 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ |
67 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ |