inductive ProofWidgets.Svg.ActionKind : Type

• timeout: ProofWidgets.Svg.ActionKind
• mousedown: ProofWidgets.Svg.ActionKind
• mouseup: ProofWidgets.Svg.ActionKind
• mousemove: ProofWidgets.Svg.ActionKind

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 : ProofWidgets.Svg.ActionKind.toCtorIdx x = ProofWidgets.Svg.ActionKind.toCtorIdx y then isTrue ⋯ else isFalse ⋯

structure ProofWidgets.Svg.Action : Type

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

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) : 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} → [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) : Type

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

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

• html : ProofWidgets.Html
• state : ProofWidgets.Svg.SvgState State
• callbackTime : Option Float

  Approximate number of milliseconds to wait before calling again.

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

• 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.