Raw do notation

Stream: lean4

[Calvin Lee]

How does raw do notation work? Does Id a coerce to a? Because I can't find any declaration of this in lean code

[Mario Carneiro]

do you have an example?

[Mario Carneiro]

I'm not sure what you mean by raw do notation

[Sebastian Ullrich]

Use "go to definition" :) https://github.com/leanprover/lean4/blob/master/src/Init/Control/Id.lean#L13

[Sebastian Ullrich]

(on a nightly, that is)

[Calvin Lee]

Oh wow, i looked at that and it completely went over my head. Thank you!

[Calvin Lee]

I'm not really sure if go to def works with what I'm using (cobbled together the language server and vim) but I'll try to grep better next time

[Julian Berman]

@Calvin Lee if you feel adventurous I'd love to recruit another person or two to build out neovim support. I'm using/cobbling together https://github.com/Julian/lean.nvim/

[Calvin Lee]

Oh sure! I've been using lean4 pretty comfortably with neovim (albeit using CoC instead of native lsp) I could try to add support if you'd like

[Julian Berman]

Yeah I was planning on adding "use whichever LSP support you'd like" to it, since I too used to use coc

[Julian Berman]

so certainly would love that

[Julian Berman]

(I can confirm by the way that go to definition works just fine on lean 4 with my setup and a lean 4 nightly)

[Calvin Lee]

Oh! it does indeed
I was updating nightly wrong, so I was a little more than a week behind on lean4 :sweat_smile:

[Alex J. Best]

I'm also happy to help, I was using your neovim plugin occasionally for lean 3 already @Julian Berman so thanks for that!

[Julian Berman]

@Alex J. Best oh, amazing! Please do

[Julian Berman]

sorry that I haven't documented it too well yet

[Johan Commelin]

@Julian Berman out of curiosity, do you plan to support widgets in neovim? If so, how?