15-814 LaTeX help

Here follow some helpful commands for type theory:

• \infer This command creates inference rules. It takes two arguments: in order, the conclusion, and the premises separated by ampersands. Thus, \infer{R}{P & Q} derives R from the premises P and Q. It can be nested; each of the premises can itself be an \infer. It also takes an optional argument allowing you to name the rule: \infer[int0]{0 : int}{} allows you to prove that 0 is an int under any conditions by the rule int0.
• The LaTeX Symbol List may come in handy; however, I recommend downloading and saving it because it's several meg in size. Relatedly, it's not recommendable to print the whole thing out; CTAN has more compact versions but I can't find them right now.
• Some particular commands that will come in handy very shortly, since you probably don't feel like trawling through the comprehensive list for them: \lambda, \vdash, \mapsto, \Downarrow; this should get you started.