feat: add Html type - #14935
Conversation
|
The adaptation PR for this PR is leanprover/downstream-lean4#25. |
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
|
|
||
| instance : Coe String Html := ⟨.text⟩ | ||
|
|
||
| /-- Append two HTML forests. -/ |
There was a problem hiding this comment.
| /-- Append two HTML forests. -/ | |
| /-- Appends two HTML forests. -/ |
Indicative mood
| /-- Merges an array of HTML values by appending them. | ||
|
|
||
| Equivalent to {name}`Html.seq`, but may produce a more compact representation. -/ | ||
| def ofArray (hs : Array Html) : Html := Id.run do |
There was a problem hiding this comment.
Should this work for anything with a ForIn instance? Akin to insertMany?
| letI : Quote Html `term := ⟨q⟩ | ||
| mkCApp ``Html.seq #[quote s] | ||
|
|
||
| /-- Visit the entire tree, applying rewrites in some monad. |
There was a problem hiding this comment.
| /-- Visit the entire tree, applying rewrites in some monad. | |
| /-- Visits the entire tree, applying rewrites in some monad. |
Though I'd probably prefer a docstring that didn't just use the same word here. A reader who doesn't know what "visting" means won't get anything out of this.
What about instead "Recursively rewrites the entire tree bottom-up." as the summary?
It would also be nice if we had more consistent naming of these operations. Syntax has rewriteBottomUpM which is like this but without the Option and replaceM which has the Option but is top-down.
|
|
||
| /-- Visit the entire tree, applying rewrites in some monad. | ||
| {name}`element` and {name}`seq` are applied post-traversal, receiving already-visited children. | ||
| Return {lean (type := "Option Html")}`none` to signal that no rewrite is to be performed. -/ |
There was a problem hiding this comment.
Does the Option help us here, vs having pure as the default implementation?
3 participants
Downstream adoption (not merely adaptation to make CI pass) PRs: