inductive ProofWidgets.Svg.ActionKind : Type

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

def ProofWidgets.Svg.instToJsonActionKind.toJson : ActionKind → Lean.Json

Equations

• ProofWidgets.Svg.instToJsonActionKind.toJson ProofWidgets.Svg.ActionKind.timeout = Lean.toJson "timeout"
• ProofWidgets.Svg.instToJsonActionKind.toJson ProofWidgets.Svg.ActionKind.mousedown = Lean.toJson "mousedown"
• ProofWidgets.Svg.instToJsonActionKind.toJson ProofWidgets.Svg.ActionKind.mouseup = Lean.toJson "mouseup"
• ProofWidgets.Svg.instToJsonActionKind.toJson ProofWidgets.Svg.ActionKind.mousemove = Lean.toJson "mousemove"

instance ProofWidgets.Svg.instToJsonActionKind : Lean.ToJson ActionKind

Equations

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

def ProofWidgets.Svg.instFromJsonActionKind.fromJson : Lean.Json → Except String ActionKind

Equations

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

instance ProofWidgets.Svg.instFromJsonActionKind : Lean.FromJson ActionKind

Equations

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

instance ProofWidgets.Svg.instDecidableEqActionKind : DecidableEq ActionKind

Equations

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

structure ProofWidgets.Svg.Action : Type

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

def ProofWidgets.Svg.instToJsonAction.toJson : Action → Lean.Json

Equations

• ProofWidgets.Svg.instToJsonAction.toJson x✝ = Lean.Json.mkObj [[("kind", Lean.toJson x✝.kind)], [("id", Lean.toJson x✝.id)], [("data", Lean.toJson x✝.data)]].flatten

instance ProofWidgets.Svg.instToJsonAction : Lean.ToJson Action

Equations

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

def ProofWidgets.Svg.instFromJsonAction.fromJson : Lean.Json → Except String Action

Equations

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

instance ProofWidgets.Svg.instFromJsonAction : Lean.FromJson Action

Equations

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

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.instToJsonSvgState.toJson }

def ProofWidgets.Svg.instToJsonSvgState.toJson {State✝ : Type} [Lean.ToJson State✝] : SvgState State✝ → Lean.Json

Equations

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

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

Equations

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

def ProofWidgets.Svg.instFromJsonSvgState.fromJson {State✝ : Type} [Lean.FromJson State✝] : Lean.Json → Except String (SvgState State✝)

Equations

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

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.instToJsonUpdateParams.toJson }

def ProofWidgets.Svg.instToJsonUpdateParams.toJson {State✝ : Type} [Lean.ToJson State✝] : UpdateParams State✝ → Lean.Json

Equations

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

def ProofWidgets.Svg.instFromJsonUpdateParams.fromJson {State✝ : Type} [Lean.FromJson State✝] : Lean.Json → Except String (UpdateParams State✝)

Equations

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

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

Equations

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

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.