inductive ProofWidgets.Svg.ActionKind : Type

• timeout : ActionKind
• mousedown : ActionKind
• mouseup : ActionKind
• mousemove : ActionKind

instance ProofWidgets.Svg.instToJsonActionKind : Lean.ToJson ActionKind

Equations

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

instance ProofWidgets.Svg.instFromJsonActionKind : Lean.FromJson ActionKind

Equations

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

instance ProofWidgets.Svg.instDecidableEqActionKind : DecidableEq ActionKind

Equations

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

structure ProofWidgets.Svg.Action : Type

• kind : ActionKind
• id : Option String
• data : Option Lean.Json

instance ProofWidgets.Svg.instToJsonAction : Lean.ToJson Action

Equations

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

instance ProofWidgets.Svg.instFromJsonAction : Lean.FromJson Action

Equations

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

structure ProofWidgets.Svg.SvgState (State : Type) : 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)

instance ProofWidgets.Svg.instToJsonSvgState {State✝ : Type} [Lean.ToJson State✝] : Lean.ToJson (SvgState State✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonSvgState {State✝ : Type} [Lean.FromJson State✝] : Lean.FromJson (SvgState State✝)

Equations

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

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

Equations

• ProofWidgets.Svg.instRpcEncodableSvgState = { rpcEncode := ProofWidgets.Svg.instRpcEncodableSvgState.enc✝, rpcDecode := ProofWidgets.Svg.instRpcEncodableSvgState.dec✝ }

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

• elapsed : Float
• actions : Array Action
• state : SvgState State
• mousePos : Option (Float × Float)

instance ProofWidgets.Svg.instToJsonUpdateParams {State✝ : Type} [Lean.ToJson State✝] : Lean.ToJson (UpdateParams State✝)

Equations

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

instance ProofWidgets.Svg.instFromJsonUpdateParams {State✝ : Type} [Lean.FromJson State✝] : Lean.FromJson (UpdateParams State✝)

Equations

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

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

• html : Html
• state : SvgState State
• callbackTime : Option Float

  Approximate number of milliseconds to wait before calling again.

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

Equations

• ProofWidgets.Svg.instRpcEncodableUpdateResult = { rpcEncode := ProofWidgets.Svg.instRpcEncodableUpdateResult.enc✝, rpcDecode := ProofWidgets.Svg.instRpcEncodableUpdateResult.dec✝ }

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

• init : State
• frame : Frame
• update (time_ms Δt_ms : Float) (action : Action) (mouseStart mouseEnd : Option (Point self.frame)) (selectedId : Option String) (getSelectedData : (α : Type) → [Lean.FromJson α] → Option α) : State → State
• render (time_ms : Float) (mouseStart mouseEnd : Option (Point self.frame)) : State → Svg self.frame

def ProofWidgets.Svg.InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State) (params : UpdateParams State) : Lean.Server.RequestM (Lean.Server.RequestTask (UpdateResult State))

Equations

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