Documentation

ProofWidgets.Data.Html

We define a representation of HTML trees together with a JSX-like DSL for writing them.

A HTML tree which may contain widget components.

Instances For
    def ProofWidgets.Html.ofComponent {Props : Type} [Lean.Server.RpcEncodable Props] (c : Component Props) (props : Props) (children : Array Html) :
    Equations
      Instances For

        See MDN docs.

        Instances For
          Equations
            Instances For

              Interpolates an expression into a JSX attribute literal.

              Equations
                Instances For

                  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
                    Instances For

                      Characters not allowed inside JSX plain text.

                      Equations
                        Instances For

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

                          Equations
                            Instances For
                              def ProofWidgets.Jsx.getJsxText :
                              Lean.TSyntax `ProofWidgets.Jsx.jsxTextString
                              Equations
                                Instances For

                                  Interpolates an array of elements into a JSX literal

                                  Equations
                                    Instances For

                                      Interpolates an expression into a JSX literal

                                      Equations
                                        Instances For
                                          Equations
                                            Instances For

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

                                              Equations
                                                Instances For

                                                  Now wrap our TSyntax _ delaborators into Term elaborators.