Lambda the Ultimate

LtU now supports MathJax, which allows the use of TeX markup in posts and comments. Note that only TeX/LaTeX markup is currently supported - the alternate MathML format conflict's with the blog's HTML sanitization.

This enhancement is dedicated to neelk, who most recently suggested this feature just over a year ago.

When I went searching for a bit of Mathjax-compatible LaTeX that was relevant to programming languages, the first good example Google found for me was on Neel's blog:

$$
\newcommand{\val}[1]{\mathsf{val}\,{#1}}
\newcommand{\rule}[2]{\frac{\array{#1}}{#2}}
\newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}
\newcommand{\letv}[3]{\mathsf{let}\;{#1} = {#2}\;\mathsf{in}\;{#3}}
\begin{array}{ll}
\rule{\judge{\Gamma}{e}{A}}
{\judge{\Gamma}{\val{e}}{T(A)}}
&
\rule{\judge{\Gamma}{e}{T(A)} \qquad
\judge{\Gamma, x:A}{e'}{T(C)}}
{\judge{\Gamma}{\letv{\val{x}}{e}{e'}}{T(C)}}
\end{array}
$$

Copy-pasting the above and making it work immediately made it clear that we're going to need a package of useful macros. But it's a start. Feedback welcome.

Note that MathJax rendering is entirely client-side - if you don't see a well-formatted formula above, check the MathJax browser compatibility page and their FAQ.