Equations
Equations
- ProofWidgets.Svg.instFromJsonFrame = { fromJson? := ProofWidgets.Svg.fromJsonFrame✝ }
Equations
Equations
- ProofWidgets.Svg.instFromJsonColor = { fromJson? := ProofWidgets.Svg.fromJsonColor✝ }
Equations
Equations
Equations
- ProofWidgets.Svg.instFromJsonPoint = { fromJson? := ProofWidgets.Svg.fromJsonPoint✝ }
Equations
- (ProofWidgets.Svg.Point.abs x y).toAbsolute = (x, y)
- (ProofWidgets.Svg.Point.px i j).toAbsolute = (f.xmin + (Int.toFloat✝ i + 0.5) * f.pixelSize, f.ymax - (Int.toFloat✝ j + 0.5) * f.pixelSize)
Instances For
Equations
Equations
- ProofWidgets.Svg.instFromJsonSize = { fromJson? := ProofWidgets.Svg.fromJsonSize✝ }
- line {f : Frame} (src trg : Point f) : Shape f
- circle {f : Frame} (center : Point f) (radius : Size f) : Shape f
- polyline {f : Frame} (points : Array (Point f)) : Shape f
- polygon {f : Frame} (points : Array (Point f)) : Shape f
- path {f : Frame} (d : String) : Shape f
- ellipse {f : Frame} (center : Point f) (rx ry : Size f) : Shape f
- rect {f : Frame} (corner : Point f) (width height : Size f) : Shape f
- text {f : Frame} (pos : Point f) (content : String) (size : Size f) : Shape f
Instances For
Equations
Equations
- ProofWidgets.Svg.instFromJsonShape = { fromJson? := ProofWidgets.Svg.fromJsonShape✝ }
Equations
Equations
def
ProofWidgets.Svg.Element.setData
{α : Type}
{f : Frame}
(elem : Element f)
(a : α)
[Lean.ToJson α]
:
Element f
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
- ProofWidgets.Svg.line p q = { shape := ProofWidgets.Svg.Shape.line p q }
Instances For
Equations
- ProofWidgets.Svg.circle c r = { shape := ProofWidgets.Svg.Shape.circle c r }
Instances For
Equations
- ProofWidgets.Svg.polyline pts = { shape := ProofWidgets.Svg.Shape.polyline pts }
Instances For
Equations
- ProofWidgets.Svg.polygon pts = { shape := ProofWidgets.Svg.Shape.polygon pts }
Instances For
Equations
- ProofWidgets.Svg.path d = { shape := ProofWidgets.Svg.Shape.path d }
Instances For
Equations
- ProofWidgets.Svg.ellipse center rx ry = { shape := ProofWidgets.Svg.Shape.ellipse center rx ry }
Instances For
Equations
- ProofWidgets.Svg.rect corner width height = { shape := ProofWidgets.Svg.Shape.rect corner width height }
Instances For
Equations
- ProofWidgets.Svg.text pos content size = { shape := ProofWidgets.Svg.Shape.text pos content size }
Instances For
def
ProofWidgets.mkIdToIdx
{f : Svg.Frame}
(elements : Array (Svg.Element f))
:
Std.HashMap String (Fin elements.size)
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
- svg.idToData = Std.HashMap.ofList svg.idToDataList