[Agda] Re: Possible bug when using "with" on a partially applied function

Christopher Jenkins cjenkin1 at trinity.edu
Mon Nov 24 01:21:40 CET 2014


On Sun, Nov 23, 2014 at 4:39 PM, Christopher Jenkins <cjenkin1 at trinity.edu>
wrote:

> However, this is *not* that situation here. Agda has mysteriously eaten n
> : Nat, and replaced its occurrences with *a : A* (a parametric type),
> generating a type error.
>

Should be: *x : A* (a parametric type)


-- 
Christopher Jenkins
Computer Science 2013
Trinity University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141123/5a82d6ca/attachment.html


More information about the Agda mailing list