I think my settings are wrong. - 'idris.typecheck'

[DUVELA]

I can a little understand English. I use a translator so it's ok.

OS : windows 10 C:\Program Files\Microsoft VS Code. C:\Users\i.vscode\extensions |ms-vscode.atom-keybindings-3.0.2 | vscode-idris-master | zjhmale.idris-0.9.8

I can see that it works. "idris.add-clause", keybinding - Ctrl + Alt + A "idris.case-split", keybinding - Ctrl + Alt + C "idris.docs-for", keybinding - Ctrl + Alt + D "idris.make-lemma", keybinding - Ctrl + Alt + L "idris.make-case", keybinding - Ctrl + Alt + M "idris.proof-search", keybinding - Ctrl + Alt + S "idris.type-of", keybinding - Ctrl + Alt + T

"idris.typecheck".. um.... hello??? "idris.typecheck" is no response.

what is a problem? I wanna see that "file loaded successfully" or error message.

[corazza]

Yeah it seems like the command isn't working: https://github.com/zjhmale/vscode-idris/issues/118

Which is too bad I really wanted to switch to VS Code, but I can't stand when trivial stuff doesn't work:)

[DUVELA]

Well ... I was forgetting vscode because I could not solve it. :)