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

[Andreas Abel]

Issue acknowledged:

   https://code.google.com/p/agda/issues/detail?id=1369

Note that "with" on an expression of function type is rather pointless, 
as you can only match on data, not on functions.  But surely, Agda 
should make a more graceful exit in this case.

On 24.11.2014 01:21, Christopher Jenkins wrote:
> On Sun, Nov 23, 2014 at 4:39 PM, Christopher Jenkins
> <cjenkin1 at trinity.edu <mailto: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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/