I’m trying out VSCode, and pleasantly surprised to find there’s a nice interactive @idrislang mode for it. Thanks!https://github.com/zjhmale/vscode-idris …
-
-
We should steal the interaction server design from Lean, they did it very nicely
-
We evaluated using LSP when we rewrote Lean's interactive protocol, but even for the few commands where it's a good fit the benefits are so small
- 3 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.