I'd actually love to see a demonstration of someone effectively using them. Anyone know of such a recording?
Conversation
Not sure… I can't remember how I learned in the past… I know somehow along the line I learned how you could plonk stuff in the hole and then run a command to case split or proof search based on that stuff…? Been a while since I goofed about with Agda and am far from an expert.
1
I just searched on youtube and maybe this one?
1
2
It's just a intro tutorial though so probably not illustrative of more advanced cases.
I also think I recall seeing people also being able to extend the hole commands with custom tactics as well, but not sure how common that is.
1
But yeah, shows how you use the hole to direct splitting and refining the state of the program. So you end up sort of… pushing around holes in order to build up your program… uhh proof.
1
I think having some scratch space is useful in the hole (they seem to call it a ‘shed’?) because it lets you give more info for the specific command you want to run. But yeah, as I say it’s been a while since I messed with it.
1
1
would be curious how this could work with a more “continuous” style of editing. Maybe in the hole you could write some sort of ‘hole tactic’ (that you’ve perhaps brought into scope in your editor, like “split” or “refine”) in the hole and it could prompt for info as you type.
2
This sounds like you want edit-time tactics, which already exist in Idris (and in a more primitive form in Agda)
1
2
Oh maybe that’s what I was thinking of. I’m sure I saw a talk video where someone put a tactic in the hole and used it to generate stuff in Agda. 😅
1
Like maybe it doesn’t have to be that advanced but I’m always thinking ‘whats a more general thing’, eg. As opposed to a bunch of hard coded tactic keywords you could type into the hole.
1
I’d imagine you could also tie that in with the default autosuggest feature most editors have which could help remind people if they forget.