Holes really confuse students, especially the interface for filling them, and especially the general lack of reasonable Mac compatibility. I'd way rather have no holes, though some nice mouse-over annotations would be useful still. Or maybe a dramatically different hole interface
Conversation
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
1
3
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
Good support for continuous editing should not require any explicit action from the user at all
2
4
Yeah the continuous editing in Lean is something I love so much! I love it how things live update as I do stuff, but maybe I’m just used to that from other languages… I generally use source control if I want to remember a past state.
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Ahhh yeah that sounds like a massive pain
1
1
Show replies
I also love how you can just click on tactics and see the implementation - really helps to demystify some of the magic, beyond them just being some black box. The structured tactics that Lean 4 was also exploring last time I looked seemed like a nice improvement too.
1
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies