Labels

• bug

  Something isn't working
• chore

  Something which should be addressed. also small bugs with little to no impact
• depends-on-external-issue
• documentation

  Improvements or additions to documentation
• duplicate

  This issue or pull request already exists
• enhancement

  New feature or request
• future-ideas

  Maintainers will not work on this but PR welcome!
• invalid

  This doesn't seem right
• lean4monaco-update

  Changes required in future lean4monaco or vscode-lean4 update
• not-reproduced

  Could not be reproduced. More details may be needed
• question

  A question which does not immediately call for action/changes