Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

UserWidget #152

Open
Seasawher opened this issue Nov 17, 2024 · 2 comments
Open

UserWidget #152

Seasawher opened this issue Nov 17, 2024 · 2 comments
Labels
doc-request Request for missing documenation

Comments

@Seasawher
Copy link

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.
@Seasawher Seasawher added the doc-request Request for missing documenation label Nov 17, 2024
@david-christiansen
Copy link
Collaborator

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
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
doc-request Request for missing documenation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@david-christiansen @Seasawher