Zulip Chat Archive

Stream: lean4

Topic: tab completion?

Jason Gross (Mar 22 2021 at 18:33):

Is there an editor with tab completion for Lean? (Is there a way to get tab completion in lean4-mode for emacs?) Especially, can there be tab-completion for set_option?

Bryan Gin-ge Chen (Mar 22 2021 at 18:41):

I believe this has not been implemented yet.

Last updated: Dec 20 2023 at 11:08 UTC