[Agda] New: Syntax for let pattern bindings

[Andreas Abel]

On 05.06.12 7:52 PM, Wolfram Kahl wrote:
> On Tue, Jun 05, 2012 at 04:22:51PM +0200, Andreas Abel wrote:
>>
>> I am proud to announce a small addition to Agda syntax.  Record patterns
>> can now be bound to values with a 'let'.
>>
>
> YES!! THANK YOU!!!

Thanks for saying "Thank you". :)

>> A better internal handling of let-bindings that would allow the treatment
>>
>>    let t  = splitAt n xs
>>        ys = proj₁ t
>>        zs = proj₂ t
>>    in  ...
>>
>> is an open issue.
>
> Open in which sense?
>
>   * Unknown whether possible (in general)?
>   * Considered possible, but not planned?
>   * Easy, but just not done yet?

Well, it would require quite a bit of restructuring of Agda's Internal 
syntax.

Be welcome to discuss this on the bug tracker at

   http://code.google.com/p/agda/issues/detail?id=514

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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