-
Notifications
You must be signed in to change notification settings - Fork 22
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: implement JSX ...
notation
#54
feat: implement JSX ...
notation
#54
Conversation
1745e3a
to
46e928e
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, thank you!
ProofWidgets/Data/Html.lean
Outdated
/-- Interpolates an expression into a JSX literal -/ | ||
scoped syntax "{" term "}" : jsxChild | ||
scoped syntax jsxElement : jsxChild | ||
|
||
scoped syntax:max jsxElement : term | ||
|
||
def transformTag (n m : Ident) (ns : Array Ident) (vs : Array (TSyntax `jsxAttrVal)) | ||
/-- Sends `#[a, b, c]` to `` `(term| $a ++ $b ++ $c)``-/ | ||
def joinArrays {m} [Monad m] [MonadRef m] [MonadQuotation m] (arr : Array Term) : m Term := do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could we move the general functions such as joinArrays
/foldInlsM
/delabListLiteral
/... to a ProofWidgets.Util
module?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've moved the new ones in this PR.
This makes
<tag {...atts}>{...children}</tag>
work, and adds support in the delaborator.The delaborator prints
<tag foo={1} {...attrs}><child />{...children}</tag>
in a suboptimal way, but it's better than it was before.