[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