elabStringDiagramCmd — Mathlib

Lean4
@[command_elab stringDiagram, inherit_doc stringDiagram]
def elabStringDiagramCmd : CommandElab := fun
  | stx@(`(#string_diagram $t:term)) => do
    let html ←
      runTermElabM fun _ => do
          let e ←
            try
              mkConstWithFreshMVarLevels (← realizeGlobalConstNoOverloadWithInfo t)
            catch _ =>
              Term.levelMVarToParam (← instantiateMVars (← Term.elabTerm t none))
          match ← StringDiagram.stringMorOrEqM? e with
          | some html =>
            return html
          | none =>
            throwError "could not find a morphism or equality: {e}"
    liftCoreM <|
        Widget.savePanelWidgetInfo (hash HtmlDisplay.javascript)
          (return json% {html: $(← Server.RpcEncodable.rpcEncode html)}) stx
  | stx => throwError "Unexpected syntax {stx}."
Похожие утверждения