Documentation

ProofWidgets.Data.Svg

structure ProofWidgets.Svg.Frame :

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

Instances For

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) :

Equations

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

Instances For

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

Equations

frame.xmax = frame.xmin + frame.xSize

Instances For

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

Equations

frame.ymax = frame.ymin + frame.ySize

Instances For

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

Equations

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

Instances For

structure ProofWidgets.Svg.Color :

r : Float
g : Float
b : Float

Instances For

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) :

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 ")"

Instances For

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

px {f : ProofWidgets.Svg.Frame} (i j : Int) : ProofWidgets.Svg.Point f
abs {f : ProofWidgets.Svg.Frame} (x y : Float) : ProofWidgets.Svg.Point f

Instances For

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) :

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)

Instances For

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

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

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

px {f : ProofWidgets.Svg.Frame} (size : Nat) : ProofWidgets.Svg.Size f
abs {f : ProofWidgets.Svg.Frame} (size : Float) : ProofWidgets.Svg.Size f

Instances For

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) :

Equations

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

Instances For

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

line {f : ProofWidgets.Svg.Frame} (src trg : ProofWidgets.Svg.Point f) : ProofWidgets.Svg.Shape f
circle {f : ProofWidgets.Svg.Frame} (center : ProofWidgets.Svg.Point f) (radius : ProofWidgets.Svg.Size f) : ProofWidgets.Svg.Shape f
polyline {f : ProofWidgets.Svg.Frame} (points : Array (ProofWidgets.Svg.Point f)) : ProofWidgets.Svg.Shape f
polygon {f : ProofWidgets.Svg.Frame} (points : Array (ProofWidgets.Svg.Point f)) : ProofWidgets.Svg.Shape f

Instances For

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.

Instances For

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

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

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

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) }

Instances For

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.

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

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 }

Instances For

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.

Instances For

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

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

Instances For

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.

Instances For

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.

Instances For

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

Instances For

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

Instances For