Topic: emacs and contributions
Simon Hudon (Jul 25 2018 at 20:31):
I have created a
leanprover-community account on github and a
lean-mode-contrib repository. I think it will be easier to accumulate tools there and simply have members of the community maintain it than to pester the Lean developers. Other community managed repos might be useful. Feel free to make suggestions (including suggesting / volunteering maintainers)
Patrick Massot (Jul 25 2018 at 20:33):
What kind of tools do you have in mind?
Simon Hudon (Jul 25 2018 at 20:37):
So far, all I added is an emacs feature that highlights the difference between expected type and actual types in error messages
Patrick Massot (Jul 25 2018 at 22:24):
This is really nice. It's something I miss occasionally in VScode.
Last updated: May 06 2021 at 21:09 UTC