Here's the exercise (in class I added more comments about filling holes and implicit arguments and so on): dependenttyp.es/classes/fa2022
Goal is to get folks familiar with proof objects / proof terms, and with the equality type
Conversation
But have the class gets stuck figuring out the interface and doesn't have enough time to work on that. So when I ask about their experiences and how they could make it easier (it's a proof automation class), many of the answers are complaining about holes and the interface
1
2
Plus a bunch about how on a Mac, half of the keybindings don't work
4
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
VSCode doesn't seem much better than emacs for Agda honestly. Students still found it confusing and had to learn weird emacs bindings
3
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
My main problem with this is that I have to remember what the shortcut is every time I use agda (read: look it up)
1
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
The big button also means that you can hover over it to remember the shortcut. I think in editors these days if you search for the command in the command palette (Cmd+Shift+P in VS Code) it tells you the shortcut too which is helpful. Not sure about the Adga extension though.