[Agda] Location of implicit argument(s)

[Nils Anders Danielsson]

On 2009-11-20 14:38, Darin Morrison wrote:
> On 20 Nov 2009, at 12:03, Dan Licata wrote:

>> I want to write
>>
>> f (Lam (e : Term (A :: G) B)) = ...
>>
>> for
>>
>> f (Lam{G}{A}{B} e) = ...

>> Could such a syntax be made to work for Agda?

> I think this function from the standard library might do what you want:
>
> http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Function.html#2782

This function does not work in patterns. Dan seems to want to /bind/
variables using type annotations. For injective type constructors I
suppose this could be made to work, although at first sight it seems
counter-intuitive to treat a type signature as a binding construct.

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.