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

[Christopher Jenkins]

> 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.
>>
>
This was exactly my intended use case. Even though I'm not sure it would
have succeeded, the idea was to be able to change the expected argument
type of "swap" so that I could easily change the type of its given argument
"xs" in an expression containing "swap xs"


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



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