Zulip Chat Archive

Stream: lean4

Topic: Auto-completion for DSL's

Björn Fischer (May 08 2023 at 12:03):

Is it possible to extend the language server to implement auto-completion for DSL's (custom syntax categories)?

Mac Malone (May 13 2023 at 15:46):

Yes. See alloy's handleCompletion function for a partial example (the code is flaky, but it does demonstrate well what can be done).

Last updated: May 02 2025 at 03:31 UTC