def ProofWidgets.Jsx.proofWidgetsJsxElement.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.proofWidgetsJsxElement : Category

Equations

• Lean.Parser.Category.proofWidgetsJsxElement = { }

def Lean.Parser.Category.proofWidgetsJsxChild : Category

Equations

• Lean.Parser.Category.proofWidgetsJsxChild = { }

def ProofWidgets.Jsx.proofWidgetsJsxChild.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.proofWidgetsJsxAttr.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.proofWidgetsJsxAttr : Category

Equations

• Lean.Parser.Category.proofWidgetsJsxAttr = { }

def ProofWidgets.Jsx.proofWidgetsJsxAttrVal.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.proofWidgetsJsxAttrVal : Category

Equations

• Lean.Parser.Category.proofWidgetsJsxAttrVal = { }

def ProofWidgets.Jsx.proofWidgetsJsxAttrVal_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.proofWidgetsJsxAttrVal_ = Lean.ParserDescr.node `ProofWidgets.Jsx.proofWidgetsJsxAttrVal_ 1022 (Lean.ParserDescr.const `str)

def ProofWidgets.Jsx.«proofWidgetsJsxAttrVal{_}» : Lean.ParserDescr

Interpolates an expression into a JSX attribute literal.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.«proofWidgetsJsxAttr_=_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.«proofWidgetsJsxAttr{..._}» : Lean.ParserDescr

Interpolates a collection into a JSX attribute literal. For HTML tags, this should have type Array (String × Json). For ProofWidgets.Components, it can be any structure $t whatsoever: it is interpolated into the component's props using { $t with ... } notation.

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.jsxTextForbidden : String

Characters not allowed inside JSX plain text.

Equations

• ProofWidgets.Jsx.jsxTextForbidden = "{<>}$"

def ProofWidgets.Jsx.jsxText : Lean.Parser.Parser

A plain text literal for JSX (notation for Html.text).

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.getJsxText : Lean.TSyntax `ProofWidgets.Jsx.jsxText → String

Equations

• ProofWidgets.Jsx.getJsxText x✝ = x✝.raw[0].getAtomVal

def ProofWidgets.Jsx.jsxText.formatter : Lean.PrettyPrinter.Formatter

Equations

• ProofWidgets.Jsx.jsxText.formatter = Lean.PrettyPrinter.Formatter.visitAtom `ProofWidgets.Jsx.jsxText

def ProofWidgets.Jsx.jsxText.parenthesizer : Lean.PrettyPrinter.Parenthesizer

Equations

• ProofWidgets.Jsx.jsxText.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def ProofWidgets.Jsx.«proofWidgetsJsxElement<__/>» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.«proofWidgetsJsxElement<__>_</_>» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.proofWidgetsJsxChild_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.proofWidgetsJsxChild_ = Lean.ParserDescr.node `ProofWidgets.Jsx.proofWidgetsJsxChild_ 1022 (Lean.ParserDescr.parser `ProofWidgets.Jsx.jsxText)

def ProofWidgets.Jsx.«proofWidgetsJsxChild{..._}» : Lean.ParserDescr

Interpolates an array of elements into a JSX literal

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.«proofWidgetsJsxChild{_}» : Lean.ParserDescr

Interpolates an expression into a JSX literal

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.proofWidgetsJsxChild__1 : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.proofWidgetsJsxChild__1 = Lean.ParserDescr.node `ProofWidgets.Jsx.proofWidgetsJsxChild__1 1022 (Lean.ParserDescr.cat `proofWidgetsJsxElement 0)

def ProofWidgets.Jsx.term_ : Lean.ParserDescr

Equations

• ProofWidgets.Jsx.term_ = Lean.ParserDescr.node `ProofWidgets.Jsx.term_ 1024 (Lean.ParserDescr.cat `proofWidgetsJsxElement 0)

def ProofWidgets.Jsx.transformTag (tk : Lean.Syntax) (n m : Lean.Ident) (vs : Array (Lean.TSyntax `proofWidgetsJsxAttr)) (cs : Array (Lean.TSyntax `proofWidgetsJsxChild)) : Lean.MacroM Lean.Term

Equations

• One or more equations did not get rendered due to their size.

First delaborate into our non-term TSyntax. Note this means we can't call delab, so we have to add the term annotations ourselves.

def ProofWidgets.Jsx.delabHtmlText : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `ProofWidgets.Jsx.jsxText)

Equations

• One or more equations did not get rendered due to their size.

partial def ProofWidgets.Jsx.delabHtmlElement' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `proofWidgetsJsxElement)

partial def ProofWidgets.Jsx.delabHtmlOfComponent' : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `proofWidgetsJsxElement)

partial def ProofWidgets.Jsx.delabJsxChildren : Lean.PrettyPrinter.Delaborator.DelabM (Array (Lean.TSyntax `proofWidgetsJsxChild))

Now wrap our TSyntax _ delaborators into Term elaborators.

def ProofWidgets.Jsx.delabHtmlElement : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.Jsx.delabHtmlOfComponent : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.