<div dir="ltr">Hello Bradley,<div><br></div><div>This is really a neat-looking library!</div><div><br></div><div>I think the idea of holes is very clever and probably has other interesting uses as well. For example, it turns any expression into a (function, point) pair. E.g., <span style="font-size:12.8px">⌞ 1 ⌟ + 2 becomes (</span><span style="font-size:12.8px">λ x → x + 2, 1). This could be used for example to apply a functor.</span></div><div><br></div><div>Best,</div><div>Owen</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 27, 2017 at 2:01 PM, Victor Miraldo <span dir="ltr"><<a href="mailto:v.cacciarimiraldo@gmail.com" target="_blank">v.cacciarimiraldo@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Bradley,<br>
<span class=""><br>
> 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.<br>
<br>
</span>This is all easier if you have a simpler intermediate language than<br>
full blown agda. We managed<br>
to get away with one possible hole only, but we could only handle a<br>
subset of agda.<br>
Infering the parameters is also simple if you control unification, but<br>
we always had the<br>
cumbersome overhead of having an intermediate term language to deal with.<br>
(which is fairly significant!)<br>
<br>
Nervetheless, great work! I still find myself writing boring congs and substs on<br>
my equational proofs. I'll keep an eye in your library!<br>
<br>
Best,<br>
<div class="HOEnZb"><div class="h5">Victor<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>