Support for LaTeX

[Vtec234]

At IPAM this year, Patrick Massot and Kyle Miller presented a demo of programmatic informalization of Lean proofs. Their software outputs an interactive webpage with both goal states and the proof displayed as English/LaTeX.

This issue is to investigate whether the same infrastructure (in particular, registering "here is how to pretty-print this kind of expression") could be shared to display LaTeX in Lean goals in the infoview. In order to render expressions, ProofWidgets could invoke a typeclass-driven or attribute-driven system similar to Massot/Miller's from an ExprPresenter with layoutKind := .inline. Using general Expr presentation mechanisms (see #4), the resulting HTML could then be shown in a tactic state display.