Zulip Chat Archive

Stream: new members

Topic: associativity of infix operators


Mike Shulman (Oct 11 2022 at 15:43):

Thanks! I don't suppose any of this works for Emacs?

Patrick Massot (Oct 11 2022 at 15:50):

I don't know anything about emacs. I know some of it works for vim.

Adam Topaz (Oct 11 2022 at 16:05):

It doesn't work for emacs unfortunately, or at least it didn't last time I tried.

Adam Topaz (Oct 11 2022 at 16:07):

I wish the emacs package (for both Lean3 and 4) got more love :(

Julian Berman (Oct 11 2022 at 17:31):

I think we need to coordinate slightly better (at least emacs + vim) to find some ways to reduce duplication

Julian Berman (Oct 11 2022 at 17:33):

I don't have a ton of Lean time myself at the minute but when we were learning about implementing widgets for neovim was probably a decent time to try to do it for both with possibly only a bit more effort but that would have involved learning enough about lean-mode that made it not happen

Julian Berman (Oct 11 2022 at 17:34):

And some things would likely be useful for both -- e.g. porting tailwind.css to something usable in a terminal is something we only partially did, and I don't know whether there's a decent way to do so that'd work for both editors but certainly we should think about those things -- or think about thinking about them :P

Julian Berman (Oct 11 2022 at 17:35):

Sorry, tachyons, not tailwind, too many css frameworks on the mind.

Adam Topaz (Oct 11 2022 at 17:42):

A hacky but (presumably) simple solution would be to display widgets in an external browser window.

Julian Berman (Oct 11 2022 at 17:44):

yeah -- I put a link to a thing for neovim which does so in https://github.com/Julian/lean.nvim/issues/59

Julian Berman (Oct 11 2022 at 17:45):

who knows how much brain is left for lean 3 from folks but maybe that's even possible to share with emacs if we somehow do it in the language server (like have the language server process drive the browser window) but that's random speculating without rethinking about it


Last updated: Dec 20 2023 at 11:08 UTC