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 Frame

Equations

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

instance ProofWidgets.Svg.instFromJsonFrame :

Lean.FromJson Frame

Equations

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

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

Equations

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

Instances For

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

Equations

frame.xmax = frame.xmin + frame.xSize

Instances For

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

Equations

frame.ymax = frame.ymin + frame.ySize

Instances For

def ProofWidgets.Svg.Frame.pixelSize (frame : 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 Color

Equations

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

instance ProofWidgets.Svg.instFromJsonColor :

Lean.FromJson Color

Equations

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

instance ProofWidgets.Svg.instCoeProdFloatColor :

Coe (Float × Float × Float) 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 : 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 : Frame) :

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

Instances For

instance ProofWidgets.Svg.instInhabitedPoint {a✝ : Frame} :

Inhabited (Point a✝)

Equations

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

instance ProofWidgets.Svg.instToJsonPoint {f✝ : Frame} :

Lean.ToJson (Point f✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonPoint {f✝ : Frame} :

Lean.FromJson (Point f✝)

Equations

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

instance ProofWidgets.Svg.instCoeProdFloatPoint (f : Frame) :

Coe (Float × Float) (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 : Frame) :

Coe (Int × Int) (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 : Frame} (p : 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 : Frame} (p : 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 : Frame) :

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

Instances For

instance ProofWidgets.Svg.instToJsonSize {f✝ : Frame} :

Lean.ToJson (Size f✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonSize {f✝ : Frame} :

Lean.FromJson (Size f✝)

Equations

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

def ProofWidgets.Svg.Size.toPixels {f : Frame} (s : 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 : Frame) :

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

Instances For

instance ProofWidgets.Svg.instToJsonShape {f✝ : Frame} :

Lean.ToJson (Shape f✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonShape {f✝ : Frame} :

Lean.FromJson (Shape f✝)

Equations

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

def ProofWidgets.Svg.Shape.toHtmlData {f : Frame} :

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

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

Instances For

instance ProofWidgets.Svg.instToJsonElement {f✝ : Frame} :

Lean.ToJson (Element f✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonElement {f✝ : Frame} :

Lean.FromJson (Element f✝)

Equations

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

def ProofWidgets.Svg.Element.setStroke {f : Frame} (elem : Element f) (color : Color) (width : Size 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 : Frame} (elem : Element f) (color : Color) :

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 : Frame} (elem : Element f) (id : String) :

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 : Frame} (elem : Element f) (a : α) [Lean.ToJson α] :

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 : Frame} (e : Element f) :

Equations

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

Instances For

def ProofWidgets.Svg.line {f : Frame} (p q : Point 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 : Frame} (c : Point f) (r : Size 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 : Frame} (pts : Array (Point 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 : Frame} (pts : Array (Point 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 : 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

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

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

Instances For

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

Equations

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

Instances For

def ProofWidgets.Svg.idToDataList {f : Frame} (svg : 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 : Frame} (svg : Svg f) :

Std.HashMap String Lean.Json

Equations

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

Instances For

instance ProofWidgets.Svg.instGetElemNatElementLtSizeElements {f : Frame} :

GetElem (Svg f) Nat (Element f) fun (svg : 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 : Frame} :

GetElem (Svg f) String (Option (Element f)) fun (x : Svg f) (x : String) => True

Equations

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

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

Option Lean.Json

Equations

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

Instances For