leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: try this for emacs


Simon Hudon (Jul 09 2020 at 15:00):

I believe some work was done to get VS code to read advice written as "try this" and apply it. Was it ever implemented in emacs?

Patrick Massot (Jul 09 2020 at 15:14):

As far as I know, nobody is actively working on the emacs Lean mode.

Simon Hudon (Jul 09 2020 at 15:16):

Any idea how the VS code implementation works?


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll