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

[Andreas Abel]

Fixed this issue just now.

On 25.11.2014 17:42, Andrea Vezzosi wrote:
> 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)

-- 
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/