search

leanprover / reference-manual

Apache License 2.0
26 stars 3 forks source link

UserWidget #152

Open Seasawher opened 1 week ago

Seasawher commented 1 week ago

What question should the reference manual answer?

Usage and implementation of UserWidget.

Additional context

The Lean Manual contained a description of this, but this new manual does not yet.

david-christiansen commented 1 week ago

The old description of this feature isn't going anywhere - don't worry!

When it comes time to document this in the new language reference, what specific aspects are most valuable for your work? There's the RPC interface to the language server, the JavaScript API provided by the Infoview, build/distribution issues, and many other aspects. Are any of these more important than the others for your work?

Seasawher commented 1 week ago

I am relieved to hear that Lean Manual is not going away.

I would like to learn more about widgets, because with them I can do numerical calculations in Lean and produce graphs.