search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

Case Split not working #105

Closed GetContented closed 2 years ago

GetContented commented 2 years ago

I did C-y C-c on a hole after loading with C-c C-l, and it doesn't recognise C-y C-c as a command.

Exact wording is "The key combination (^Y, ^C) is not a command."

I'm completely new to agda and agda-mode, FWIW, so apologies if I've done something silly.

GetContented commented 2 years ago

Ah I think this may have been because I was on the version of agda recommended by PLFA which is v2.6.1.3 as per https://plfa.github.io/GettingStarted/

However, after upgrading, case split works with C-c C-c, not with C-c C-y as the docs suggest.

GetContented commented 2 years ago

Ok so now case split isn't working again (on a different file). I typecheck, and it shows the goals, but when I type any of the goal related commands it doesn't recognise them as a command (this is from within the hole) it's also not recognising C-c C-f to go to the next hole. Super confusing.

banacorn commented 2 years ago

Oh no! I'm so sorry about this.

Case split should be and has always been C-c C-c like in Emacs. But the README somehow got it wrong.

stepchowfun commented 2 years ago

Created a PR to fix the README: https://github.com/banacorn/agda-mode-vscode/pull/111