Documentation

ProofWidgets.Component.InteractiveSvg

inductive ProofWidgets.Svg.ActionKind :

Instances For

instance ProofWidgets.Svg.instToJsonActionKind :

Lean.ToJson ProofWidgets.Svg.ActionKind

Equations

ProofWidgets.Svg.instToJsonActionKind = { toJson := ProofWidgets.Svg.toJsonActionKind✝ }

instance ProofWidgets.Svg.instFromJsonActionKind :

Lean.FromJson ProofWidgets.Svg.ActionKind

Equations

ProofWidgets.Svg.instFromJsonActionKind = { fromJson? := ProofWidgets.Svg.fromJsonActionKind✝ }

instance ProofWidgets.Svg.instDecidableEqActionKind :

DecidableEq ProofWidgets.Svg.ActionKind

Equations

ProofWidgets.Svg.instDecidableEqActionKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure ProofWidgets.Svg.Action :

Instances For

instance ProofWidgets.Svg.instToJsonAction :

Lean.ToJson ProofWidgets.Svg.Action

Equations

ProofWidgets.Svg.instToJsonAction = { toJson := ProofWidgets.Svg.toJsonAction✝ }

instance ProofWidgets.Svg.instFromJsonAction :

Lean.FromJson ProofWidgets.Svg.Action

Equations

ProofWidgets.Svg.instFromJsonAction = { fromJson? := ProofWidgets.Svg.fromJsonAction✝ }

structure ProofWidgets.Svg.SvgState (State : Type) :

The input type State is any state the user wants to use and update

SvgState in addition automatically handles tracking of time, selection and custom data

state : State
time : Float
selected : Option String
time in milliseconds
mousePos : Option (Int × Int)
idToData : List (String × Lean.Json)

Instances For

instance ProofWidgets.Svg.instToJsonSvgState :

{State : Type} → [inst : Lean.ToJson State] → Lean.ToJson (ProofWidgets.Svg.SvgState State)

Equations

ProofWidgets.Svg.instToJsonSvgState = { toJson := ProofWidgets.Svg.toJsonSvgState✝ }

instance ProofWidgets.Svg.instFromJsonSvgState :

{State : Type} → [inst : Lean.FromJson State] → Lean.FromJson (ProofWidgets.Svg.SvgState State)

Equations

ProofWidgets.Svg.instFromJsonSvgState = { fromJson? := ProofWidgets.Svg.fromJsonSvgState✝ }

instance ProofWidgets.Svg.ProofWidgets.Svg.SvgState.instFromJsonRpcEncodablePacket :

Lean.FromJson ProofWidgets.Svg.ProofWidgets.Svg.SvgState.RpcEncodablePacket✝

Equations

ProofWidgets.Svg.ProofWidgets.Svg.SvgState.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.Svg.ProofWidgets.Svg.SvgState.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.Svg.ProofWidgets.Svg.SvgState.instRpcEncodableSvgState {State : Type} [Lean.Server.RpcEncodable State] :

Lean.Server.RpcEncodable (ProofWidgets.Svg.SvgState State)

Equations

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

instance ProofWidgets.Svg.ProofWidgets.Svg.SvgState.instToJsonRpcEncodablePacket :

Lean.ToJson ProofWidgets.Svg.ProofWidgets.Svg.SvgState.RpcEncodablePacket✝

Equations

ProofWidgets.Svg.ProofWidgets.Svg.SvgState.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.Svg.ProofWidgets.Svg.SvgState.toJsonRpcEncodablePacket✝ }

structure ProofWidgets.Svg.UpdateParams (State : Type) :

elapsed : Float
actions : Array ProofWidgets.Svg.Action
state : ProofWidgets.Svg.SvgState State
mousePos : Option (Float × Float)

Instances For

instance ProofWidgets.Svg.instToJsonUpdateParams :

{State : Type} → [inst : Lean.ToJson State] → Lean.ToJson (ProofWidgets.Svg.UpdateParams State)

Equations

ProofWidgets.Svg.instToJsonUpdateParams = { toJson := ProofWidgets.Svg.toJsonUpdateParams✝ }

instance ProofWidgets.Svg.instFromJsonUpdateParams :

{State : Type} → [inst : Lean.FromJson State] → Lean.FromJson (ProofWidgets.Svg.UpdateParams State)

Equations

ProofWidgets.Svg.instFromJsonUpdateParams = { fromJson? := ProofWidgets.Svg.fromJsonUpdateParams✝ }

structure ProofWidgets.Svg.UpdateResult (State : Type) :

html : ProofWidgets.Html
state : ProofWidgets.Svg.SvgState State
callbackTime : Option Float
Approximate number of milliseconds to wait before calling again.

Instances For

ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instRpcEncodableUpdateResult

instance ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instToJsonRpcEncodablePacket :

Lean.ToJson ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.RpcEncodablePacket✝

Equations

ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instFromJsonRpcEncodablePacket :

Lean.FromJson ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.RpcEncodablePacket✝

Equations

ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.Svg.ProofWidgets.Svg.UpdateResult.instRpcEncodableUpdateResult {State : Type} [Lean.Server.RpcEncodable State] :

Lean.Server.RpcEncodable (ProofWidgets.Svg.UpdateResult State)

Equations

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

structure ProofWidgets.Svg.InteractiveSvg (State : Type) :

init : State
frame : ProofWidgets.Svg.Frame
update : Float → Float → ProofWidgets.Svg.Action → Option (ProofWidgets.Svg.Point self.frame) → Option (ProofWidgets.Svg.Point self.frame) → Option String → ((α : Type) → [inst : Lean.FromJson α] → Option α) → State → State
render : Float → Option (ProofWidgets.Svg.Point self.frame) → Option (ProofWidgets.Svg.Point self.frame) → State → ProofWidgets.Svg self.frame

def ProofWidgets.Svg.InteractiveSvg.serverRpcMethod {State : Type} (isvg : ProofWidgets.Svg.InteractiveSvg State) (params : ProofWidgets.Svg.UpdateParams State) :

Lean.Server.RequestM (Lean.Server.RequestTask (ProofWidgets.Svg.UpdateResult State))

Equations

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