structure ProofWidgets.Svg.Frame : Type

• xmin : Float
• ymin : Float
• xSize : Float
• width : Nat
• height : Nat

instance ProofWidgets.Svg.instToJsonFrame : Lean.ToJson ProofWidgets.Svg.Frame

Equations

• ProofWidgets.Svg.instToJsonFrame = { toJson := ProofWidgets.Svg.toJsonFrame✝ }

instance ProofWidgets.Svg.instFromJsonFrame : Lean.FromJson ProofWidgets.Svg.Frame

Equations

• ProofWidgets.Svg.instFromJsonFrame = { fromJson? := ProofWidgets.Svg.fromJsonFrame✝ }

def ProofWidgets.Svg.Frame.ySize (frame : ProofWidgets.Svg.Frame) : Float

Equations

• frame.ySize = frame.height.toFloat * (frame.xSize / frame.width.toFloat)

def ProofWidgets.Svg.Frame.xmax (frame : ProofWidgets.Svg.Frame) : Float

Equations

• frame.xmax = frame.xmin + frame.xSize

def ProofWidgets.Svg.Frame.ymax (frame : ProofWidgets.Svg.Frame) : Float

Equations

• frame.ymax = frame.ymin + frame.ySize

def ProofWidgets.Svg.Frame.pixelSize (frame : ProofWidgets.Svg.Frame) : Float

Equations

• frame.pixelSize = frame.xSize / frame.width.toFloat

structure ProofWidgets.Svg.Color : Type

• r : Float
• g : Float
• b : Float

instance ProofWidgets.Svg.instToJsonColor : Lean.ToJson ProofWidgets.Svg.Color

Equations

• ProofWidgets.Svg.instToJsonColor = { toJson := ProofWidgets.Svg.toJsonColor✝ }

instance ProofWidgets.Svg.instFromJsonColor : Lean.FromJson ProofWidgets.Svg.Color

Equations

• ProofWidgets.Svg.instFromJsonColor = { fromJson? := ProofWidgets.Svg.fromJsonColor✝ }

instance ProofWidgets.Svg.instCoeProdFloatColor : Coe (Float × Float × Float) ProofWidgets.Svg.Color

Equations

• ProofWidgets.Svg.instCoeProdFloatColor = { coe := fun (x : Float × Float × Float) => match x with | (r, g, b) => { r := r, g := g, b := b } }

def ProofWidgets.Svg.Color.toStringRGB (c : ProofWidgets.Svg.Color) : String

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

Equations

• c.toStringRGB = toString "rgb(" ++ toString (255 * c.r) ++ toString ", " ++ toString (255 * c.g) ++ toString ", " ++ toString (255 * c.b) ++ toString ")"

inductive ProofWidgets.Svg.Point (f : ProofWidgets.Svg.Frame) : Type

• px: {f : ProofWidgets.Svg.Frame} → Int → Int → ProofWidgets.Svg.Point f
• abs: {f : ProofWidgets.Svg.Frame} → Float → Float → ProofWidgets.Svg.Point f

instance ProofWidgets.Svg.instInhabitedPoint {a✝ : ProofWidgets.Svg.Frame} : Inhabited (ProofWidgets.Svg.Point a✝)

Equations

• ProofWidgets.Svg.instInhabitedPoint = { default := ProofWidgets.Svg.Point.px default default }

instance ProofWidgets.Svg.instToJsonPoint {f✝ : ProofWidgets.Svg.Frame} : Lean.ToJson (ProofWidgets.Svg.Point f✝)

Equations

• ProofWidgets.Svg.instToJsonPoint = { toJson := ProofWidgets.Svg.toJsonPoint✝ }

instance ProofWidgets.Svg.instFromJsonPoint {f✝ : ProofWidgets.Svg.Frame} : Lean.FromJson (ProofWidgets.Svg.Point f✝)

Equations

• ProofWidgets.Svg.instFromJsonPoint = { fromJson? := ProofWidgets.Svg.fromJsonPoint✝ }

instance ProofWidgets.Svg.instCoeProdFloatPoint (f : ProofWidgets.Svg.Frame) : Coe (Float × Float) (ProofWidgets.Svg.Point f)

Equations

• ProofWidgets.Svg.instCoeProdFloatPoint f = { coe := fun (x : Float × Float) => match x with | (x, y) => ProofWidgets.Svg.Point.abs x y }

instance ProofWidgets.Svg.instCoeProdIntPoint (f : ProofWidgets.Svg.Frame) : Coe (Int × Int) (ProofWidgets.Svg.Point f)

Equations

• ProofWidgets.Svg.instCoeProdIntPoint f = { coe := fun (x : Int × Int) => match x with | (i, j) => ProofWidgets.Svg.Point.px i j }

def ProofWidgets.Svg.Point.toPixels {f : ProofWidgets.Svg.Frame} (p : ProofWidgets.Svg.Point f) : Int × Int

Equations

• (ProofWidgets.Svg.Point.px a a_1).toPixels = (a, a_1)
• (ProofWidgets.Svg.Point.abs a a_1).toPixels = (Float.toInt ((a - f.xmin) / f.pixelSize).floor, Float.toInt ((f.ymax - a_1) / f.pixelSize).floor)

def ProofWidgets.Svg.Point.toAbsolute {f : ProofWidgets.Svg.Frame} (p : ProofWidgets.Svg.Point f) : Float × Float

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)

inductive ProofWidgets.Svg.Size (f : ProofWidgets.Svg.Frame) : Type

• px: {f : ProofWidgets.Svg.Frame} → Nat → ProofWidgets.Svg.Size f
• abs: {f : ProofWidgets.Svg.Frame} → Float → ProofWidgets.Svg.Size f

instance ProofWidgets.Svg.instToJsonSize {f✝ : ProofWidgets.Svg.Frame} : Lean.ToJson (ProofWidgets.Svg.Size f✝)

Equations

• ProofWidgets.Svg.instToJsonSize = { toJson := ProofWidgets.Svg.toJsonSize✝ }

instance ProofWidgets.Svg.instFromJsonSize {f✝ : ProofWidgets.Svg.Frame} : Lean.FromJson (ProofWidgets.Svg.Size f✝)

Equations

• ProofWidgets.Svg.instFromJsonSize = { fromJson? := ProofWidgets.Svg.fromJsonSize✝ }

def ProofWidgets.Svg.Size.toPixels {f : ProofWidgets.Svg.Frame} (s : ProofWidgets.Svg.Size f) : Nat

Equations

• (ProofWidgets.Svg.Size.px a).toPixels = a
• (ProofWidgets.Svg.Size.abs a).toPixels = (a / f.pixelSize).ceil.toUInt64.toNat

inductive ProofWidgets.Svg.Shape (f : ProofWidgets.Svg.Frame) : Type

• line: {f : ProofWidgets.Svg.Frame} → ProofWidgets.Svg.Point f → ProofWidgets.Svg.Point f → ProofWidgets.Svg.Shape f
• circle: {f : ProofWidgets.Svg.Frame} → ProofWidgets.Svg.Point f → ProofWidgets.Svg.Size f → ProofWidgets.Svg.Shape f
• polyline: {f : ProofWidgets.Svg.Frame} → Array (ProofWidgets.Svg.Point f) → ProofWidgets.Svg.Shape f
• polygon: {f : ProofWidgets.Svg.Frame} → Array (ProofWidgets.Svg.Point f) → ProofWidgets.Svg.Shape f

instance ProofWidgets.Svg.instToJsonShape {f✝ : ProofWidgets.Svg.Frame} : Lean.ToJson (ProofWidgets.Svg.Shape f✝)

Equations

• ProofWidgets.Svg.instToJsonShape = { toJson := ProofWidgets.Svg.toJsonShape✝ }

instance ProofWidgets.Svg.instFromJsonShape {f✝ : ProofWidgets.Svg.Frame} : Lean.FromJson (ProofWidgets.Svg.Shape f✝)

Equations

• ProofWidgets.Svg.instFromJsonShape = { fromJson? := ProofWidgets.Svg.fromJsonShape✝ }

def ProofWidgets.Svg.Shape.toHtmlData {f : ProofWidgets.Svg.Frame} : ProofWidgets.Svg.Shape f → String × Array (String × Lean.Json)

Equations

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

structure ProofWidgets.Svg.Element (f : ProofWidgets.Svg.Frame) : Type

• shape : ProofWidgets.Svg.Shape f
• strokeColor : Option ProofWidgets.Svg.Color
• strokeWidth : Option (ProofWidgets.Svg.Size f)
• fillColor : Option ProofWidgets.Svg.Color
• id : Option String
• data : Option Lean.Json

instance ProofWidgets.Svg.instToJsonElement {f✝ : ProofWidgets.Svg.Frame} : Lean.ToJson (ProofWidgets.Svg.Element f✝)

Equations

• ProofWidgets.Svg.instToJsonElement = { toJson := ProofWidgets.Svg.toJsonElement✝ }

instance ProofWidgets.Svg.instFromJsonElement {f✝ : ProofWidgets.Svg.Frame} : Lean.FromJson (ProofWidgets.Svg.Element f✝)

Equations

• ProofWidgets.Svg.instFromJsonElement = { fromJson? := ProofWidgets.Svg.fromJsonElement✝ }

def ProofWidgets.Svg.Element.setStroke {f : ProofWidgets.Svg.Frame} (elem : ProofWidgets.Svg.Element f) (color : ProofWidgets.Svg.Color) (width : ProofWidgets.Svg.Size f) : ProofWidgets.Svg.Element f

Equations

• elem.setStroke color width = { shape := elem.shape, strokeColor := some color, strokeWidth := some width, fillColor := elem.fillColor, id := elem.id, data := elem.data }

def ProofWidgets.Svg.Element.setFill {f : ProofWidgets.Svg.Frame} (elem : ProofWidgets.Svg.Element f) (color : ProofWidgets.Svg.Color) : ProofWidgets.Svg.Element f

Equations

• elem.setFill color = { shape := elem.shape, strokeColor := elem.strokeColor, strokeWidth := elem.strokeWidth, fillColor := some color, id := elem.id, data := elem.data }

def ProofWidgets.Svg.Element.setId {f : ProofWidgets.Svg.Frame} (elem : ProofWidgets.Svg.Element f) (id : String) : ProofWidgets.Svg.Element f

Equations

• elem.setId id = { shape := elem.shape, strokeColor := elem.strokeColor, strokeWidth := elem.strokeWidth, fillColor := elem.fillColor, id := some id, data := elem.data }

def ProofWidgets.Svg.Element.setData {α : Type} {f : ProofWidgets.Svg.Frame} (elem : ProofWidgets.Svg.Element f) (a : α) [Lean.ToJson α] : ProofWidgets.Svg.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) }

def ProofWidgets.Svg.Element.toHtml {f : ProofWidgets.Svg.Frame} (e : ProofWidgets.Svg.Element f) : ProofWidgets.Html

Equations

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

def ProofWidgets.Svg.line {f : ProofWidgets.Svg.Frame} (p q : ProofWidgets.Svg.Point f) : ProofWidgets.Svg.Element f

Equations

• ProofWidgets.Svg.line p q = { shape := ProofWidgets.Svg.Shape.line p q, strokeColor := none, strokeWidth := none, fillColor := none, id := none, data := none }

def ProofWidgets.Svg.circle {f : ProofWidgets.Svg.Frame} (c : ProofWidgets.Svg.Point f) (r : ProofWidgets.Svg.Size f) : ProofWidgets.Svg.Element f

Equations

• ProofWidgets.Svg.circle c r = { shape := ProofWidgets.Svg.Shape.circle c r, strokeColor := none, strokeWidth := none, fillColor := none, id := none, data := none }

def ProofWidgets.Svg.polyline {f : ProofWidgets.Svg.Frame} (pts : Array (ProofWidgets.Svg.Point f)) : ProofWidgets.Svg.Element f

Equations

• ProofWidgets.Svg.polyline pts = { shape := ProofWidgets.Svg.Shape.polyline pts, strokeColor := none, strokeWidth := none, fillColor := none, id := none, data := none }

def ProofWidgets.Svg.polygon {f : ProofWidgets.Svg.Frame} (pts : Array (ProofWidgets.Svg.Point f)) : ProofWidgets.Svg.Element f

Equations

• ProofWidgets.Svg.polygon pts = { shape := ProofWidgets.Svg.Shape.polygon pts, strokeColor := none, strokeWidth := none, fillColor := none, id := none, data := none }

def ProofWidgets.mkIdToIdx {f : ProofWidgets.Svg.Frame} (elements : Array (ProofWidgets.Svg.Element f)) : Std.HashMap String (Fin elements.size)

Equations

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

structure ProofWidgets.Svg (f : ProofWidgets.Svg.Frame) : Type

• elements : Array (ProofWidgets.Svg.Element f)
• idToIdx : Std.HashMap String (Fin self.elements.size)

def ProofWidgets.Svg.toHtml {f : ProofWidgets.Svg.Frame} (svg : ProofWidgets.Svg f) : ProofWidgets.Html

Equations

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

def ProofWidgets.Svg.idToDataList {f : ProofWidgets.Svg.Frame} (svg : ProofWidgets.Svg f) : List (String × Lean.Json)

Equations

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

def ProofWidgets.Svg.idToData {f : ProofWidgets.Svg.Frame} (svg : ProofWidgets.Svg f) : Std.HashMap String Lean.Json

Equations

• svg.idToData = Std.HashMap.ofList svg.idToDataList

instance ProofWidgets.Svg.instGetElemNatElementLtSizeElements {f : ProofWidgets.Svg.Frame} : GetElem (ProofWidgets.Svg f) Nat (ProofWidgets.Svg.Element f) fun (svg : ProofWidgets.Svg f) (idx : Nat) => idx < svg.elements.size

Equations

• ProofWidgets.Svg.instGetElemNatElementLtSizeElements = { getElem := fun (svg : ProofWidgets.Svg f) (i : Nat) (h : i < svg.elements.size) => svg.elements[i] }

instance ProofWidgets.Svg.instGetElemStringOptionElementTrue {f : ProofWidgets.Svg.Frame} : GetElem (ProofWidgets.Svg f) String (Option (ProofWidgets.Svg.Element f)) fun (x : ProofWidgets.Svg f) (x : String) => True

Equations

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

def ProofWidgets.Svg.getData {f : ProofWidgets.Svg.Frame} (svg : ProofWidgets.Svg f) (id : String) : Option Lean.Json

Equations

• svg.getData id = match svg[id] with | none => none | some elem => elem.data