associativity of infix operators

Stream: new members

[Mike Shulman]

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

[Patrick Massot]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Julian Berman]

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

[Julian Berman]

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]

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]

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

[Adam Topaz]

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

[Julian Berman]

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

[Julian Berman]

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