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.