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)

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

Equations

frame.xmax = frame.xmin + frame.xSize

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

Equations

frame.ymax = frame.ymin + frame.ySize

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

Equations

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

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

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

px: {f : ProofWidgets.Svg.Frame} → Int → Int → ProofWidgets.Svg.Point f
abs: {f : ProofWidgets.Svg.Frame} → Float → 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

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

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

Equations

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

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

px: {f : ProofWidgets.Svg.Frame} → Nat → ProofWidgets.Svg.Size f
abs: {f : ProofWidgets.Svg.Frame} → 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

s.toPixels = match s with | ProofWidgets.Svg.Size.px x => x | ProofWidgets.Svg.Size.abs x => (x / f.pixelSize).ceil.toUInt64.toNat

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

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

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.

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 }

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 : ProofWidgets.Svg.Point f) (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)) :

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

elements : Array (ProofWidgets.Svg.Element f)
idToIdx : Lean.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.

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

Lean.HashMap String Lean.Json

Equations

svg.idToData = Lean.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