Completions don't work with Idris2
meraymond2 opened this issue · 1 comments
meraymond2 commented
The completions reply from the client isn't correct with Idris 2. I don't have any specific notes in the client repo about that command, but presumably the output has changed, so it no longer works.
meraymond2 commented
Looked at this, and the response is (:write-string "repl-completions: command not yet implemented. Hopefully soon!" 3) so that would explain why that's not working. I've just added a note to the readme that Idris2 doesn't have completions.