equal
deleted
inserted
replaced
75 \subcaption{Binders} |
75 \subcaption{Binders} |
76 |
76 |
77 \begin{center} |
77 \begin{center} |
78 \index{*"= symbol} |
78 \index{*"= symbol} |
79 \index{&@{\tt\&} symbol} |
79 \index{&@{\tt\&} symbol} |
80 \index{*"| symbol} |
80 \index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working |
81 \index{*"-"-"> symbol} |
81 \index{*"-"-"> symbol} |
82 \index{*"<"-"> symbol} |
82 \index{*"<"-"> symbol} |
83 \begin{tabular}{rrrr} |
83 \begin{tabular}{rrrr} |
84 \it symbol & \it meta-type & \it priority & \it description \\ |
84 \it symbol & \it meta-type & \it priority & \it description \\ |
85 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ |
85 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ |