[Agda] Holes 0.1.0

[Victor Miraldo]

Hello Bradley,

> But you’re right, it would be nice to be able to do things more automatically, too, and it should definitely be doable. I could imagine building a list of ‘possible holes’ in the LHS. Then I would try to apply my macro as it stands to each of those until one type checks.

This is all easier if you have a simpler intermediate language than
full blown agda. We managed
to get away with one possible hole only, but we could only handle a
subset of agda.
Infering the parameters is also simple if you control unification, but
we always had the
cumbersome overhead of having an intermediate term language to deal with.
(which is fairly significant!)

Nervetheless, great work! I still find myself writing boring congs and substs on
my equational proofs. I'll keep an eye in your library!

Best,
Victor