dalps

I really don't see the point of this level, the Power world could very well do without it. Aside from being just math trivia, it's preventing the Power world from...

> What do you mean? I solved it with a truly remarkable proof using less than 300 lines of lean, but the GitHub comment limit is too small to contain...

Hi @voodoos, are you sure this is not merlin's responsibility? As I said, I see this error in vim too, which (correct me if I'm wrong) doesn't use the LSP...

Not a maintainer, but I believe your installation is fine. That message simply warns you that `destruct` can't infer any constructor from your pattern, or that it is already exhaustive....

Strange, I can't replicate the behavior shown by your screenshots; on my end `Alt + d` works well on your example code, however I don't get those two actions in...

Turns out I was using an older version of ocaml-lsp. After updating my installation to ocaml-lsp-server 1.18.0~5.2preview, the destruct option is no longer available through the `Alt + d` shortcut.

The install option is available from the "Manage" menu - the little cog.