Zulip Chat Archive

Stream: lean4

Topic: Raw do notation


view this post on Zulip Calvin Lee (Jan 29 2021 at 17:48):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:50):

do you have an example?

view this post on Zulip Mario Carneiro (Jan 29 2021 at 17:50):

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

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 17:53):

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

view this post on Zulip Sebastian Ullrich (Jan 29 2021 at 17:53):

(on a nightly, that is)

view this post on Zulip Calvin Lee (Jan 29 2021 at 17:57):

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

view this post on Zulip Calvin Lee (Jan 29 2021 at 17:58):

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

view this post on Zulip Julian Berman (Feb 01 2021 at 02:38):

@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/

view this post on Zulip Calvin Lee (Feb 01 2021 at 02:48):

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

view this post on Zulip Julian Berman (Feb 01 2021 at 02:49):

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

view this post on Zulip Julian Berman (Feb 01 2021 at 02:49):

so certainly would love that

view this post on Zulip Julian Berman (Feb 01 2021 at 02:50):

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

view this post on Zulip Calvin Lee (Feb 01 2021 at 02:54):

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

view this post on Zulip Alex J. Best (Feb 01 2021 at 03:02):

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

view this post on Zulip Julian Berman (Feb 01 2021 at 03:05):

@Alex J. Best oh, amazing! Please do

view this post on Zulip Julian Berman (Feb 01 2021 at 03:05):

sorry that I haven't documented it too well yet

view this post on Zulip Johan Commelin (Feb 01 2021 at 05:52):

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


Last updated: May 07 2021 at 12:15 UTC