lean4
lean4 copied to clipboard
leanprover
Widgets: `ToHtmlFormat`
As some of the Lean 3 widget features are rolling in, we should decide on the next step. I think a good one would be to provide a typeclass which will allow users to visualize types as HTML. Specifically, we would have a Html type with something like
class ToHtmlFormat (α : Type u) where
formatHtml : α → Html
On encountering a value of type which implements ToHtmlFormat, the infoview would render it as the HTML output. This is not yet the fully programmable widgets feature, but I think it will go a long way towards visualizations such as Dynkin diagrams (zulip).
@Vtec234 This is a great suggestion. Any suggestions on the type Html?
I am also wondering whether formatHtml needs to be monadic or not. What do you think?
@leodemoura Apologies about the delay; I implemented a MVP here. The type Html there is a subset of Ed's Lean 3 version which includes only the actual HTML tree structure but no programmable/virtual DOM constructors. I think a pure formatHtml is sufficient for a start. At least, I don't see a compelling use case for a monadic one (or IO) -- if one turns up later, a monadic variant could be added with an umbrella instance [ToHtmlFormat a] : ToHtmlFormatM a.
Jeremy asked me a question that made me realize you perhaps meant:
class MetaToHtmlFormat (a : Type u) where
metaFormatHtml : Expr -> MetaM Html
where the given Expr is meant to have type a. I also don't immediately see a use case for this, but we could definitely consider it if one turns up.
I also don't immediately see a use case for this, but we could definitely consider it if one turns up.
The obvious use case for the Expr version is that you can visualize terms that are noncomputable or are not closed (i.e., depend on variables in the local context).
