[Agda] Holes 0.1.0

[Owen]

Hello Bradley,

This is really a neat-looking library!

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., ⌞ 1 ⌟ + 2 becomes (λ x → x + 2, 1). This could be used for
example to apply a functor.

Best,
Owen

On Fri, Jan 27, 2017 at 2:01 PM, Victor Miraldo <v.cacciarimiraldo at gmail.com
> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170127/a4e5ec07/attachment.html>