Lean core gains an HTML type, renderer, and HTML-like syntax