[Agda] New: Syntax for let pattern bindings

[Andreas Abel]

Hi Agda crowd,

I am proud to announce a small addition to Agda syntax.  Record patterns 
can now be bound to values with a 'let'.

For instance, Data.List.splitAt can now be written as

   splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
   ...
   splitAt (suc n) (x ∷ xs) =
     let (ys , zs) = splitAt n xs
     in  (x ∷ ys , zs)

instead of using a 'with'.

Internally, this is treated as

   let ys = proj₁ (splitAt n xs)
       zs = proj₂ (splitAt n xs)
   in  ...

so be careful if you want to actually run your Agda programs.  You might 
involuntarily slip from linear into exponential time.

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.

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/