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

[Andrea Vezzosi]

On Tue, Nov 25, 2014 at 5:33 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> ...
> Note that "with" on an expression of function type is rather pointless, as
> you can only match on data, not on functions.

Sometimes with on an expression is just to have it as a variable in
the context, so that its type or itself can be rewritten by pattern
matching on other stuff.


> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda