rpc — Mathlib

Lean4
/-- The RPC method for displaying string diagrams. -/
@[server_rpc_method]
def rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
  RequestM.asTask
    (do
      let html : Option Html ←
        (do
            if props.goals.isEmpty then
              return none
            let some g := props.goals[0]? |
              unreachable!
            g.ctx.val.runMetaM { } do
                g.mvarId.withContext do
                    let type ← g.mvarId.getType
                    stringEqM? type)
      match html with
      | none =>
        return <span>No String Diagram.</span>
      | some inner =>
        return inner)
Похожие утверждения