Documentation

ProofWidgets.Data.Svg

Instances For
    Equations
    • frame.ySize = frame.height.toFloat * (frame.xSize / frame.width.toFloat)
    Instances For
      Equations
      • frame.xmax = frame.xmin + frame.xSize
      Instances For
        Equations
        • frame.ymax = frame.ymin + frame.ySize
        Instances For
          Equations
          • frame.pixelSize = frame.xSize / frame.width.toFloat
          Instances For
            Instances For
              Equations

              Returns string "rgb(r, g, b)" with r,g,b ∈ [0,...,256)

              Equations
              Instances For
                Equations
                Equations
                • ProofWidgets.Svg.instToJsonPoint = { toJson := ProofWidgets.Svg.toJsonPoint✝ }
                Equations
                • ProofWidgets.Svg.instFromJsonPoint = { fromJson? := ProofWidgets.Svg.fromJsonPoint✝ }
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • ProofWidgets.Svg.instToJsonSize = { toJson := ProofWidgets.Svg.toJsonSize✝ }
                    Equations
                    • ProofWidgets.Svg.instFromJsonSize = { fromJson? := ProofWidgets.Svg.fromJsonSize✝ }
                    Equations
                    Instances For
                      Equations
                      • ProofWidgets.Svg.instToJsonShape = { toJson := ProofWidgets.Svg.toJsonShape✝ }
                      Equations
                      • ProofWidgets.Svg.instFromJsonShape = { fromJson? := ProofWidgets.Svg.fromJsonShape✝ }
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • ProofWidgets.Svg.instToJsonElement = { toJson := ProofWidgets.Svg.toJsonElement✝ }
                        Equations
                        • ProofWidgets.Svg.instFromJsonElement = { fromJson? := ProofWidgets.Svg.fromJsonElement✝ }
                        Equations
                        • elem.setStroke color width = { shape := elem.shape, strokeColor := some color, strokeWidth := some width, fillColor := elem.fillColor, id := elem.id, data := elem.data }
                        Instances For
                          Equations
                          • elem.setFill color = { shape := elem.shape, strokeColor := elem.strokeColor, strokeWidth := elem.strokeWidth, fillColor := some color, id := elem.id, data := elem.data }
                          Instances For
                            Equations
                            • elem.setId id = { shape := elem.shape, strokeColor := elem.strokeColor, strokeWidth := elem.strokeWidth, fillColor := elem.fillColor, id := some id, data := elem.data }
                            Instances For
                              Equations
                              • elem.setData a = { shape := elem.shape, strokeColor := elem.strokeColor, strokeWidth := elem.strokeWidth, fillColor := elem.fillColor, id := elem.id, data := some (Lean.toJson a) }
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    • ProofWidgets.Svg.instGetElemNatElementLtSizeElements = { getElem := fun (svg : ProofWidgets.Svg f) (i : Nat) (h : i < svg.elements.size) => svg.elements[i] }
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Equations
                                                    • svg.getData id = match svg[id] with | none => none | some elem => elem.data
                                                    Instances For