Documentation

Lean.Widget.InteractiveDiagnostic

noncomputable def Lean.Widget.MsgEmbed.rpcPacketFor {β : outParam Type} (α : Type) [inst : Lean.Server.RpcEncoding α β] :
Equations
Equations
Equations
Equations
Equations