[Agda] Using 'let' to pattern-match on single-constructor datatypes

[Martin Stone Davis]

Should (or can) 'let' be allowed to pattern-match on single-constructor 
datatypes? As it is now, trying to use 'let' for a data constructor 
gives an error, "Expected record pattern". (See example below.)

To make it more convenient to use 'let' on product types, I issued a 
pull request on the agda-prelude 
<https://github.com/UlfNorell/agda-prelude/pull/45>, changing Σ from 
data to record. I would have preferred to leave agda-prelude as-is if 
'let' could be enhanced.

> open import Agda.Primitive
>
> infixr 1 _,_
> record Σ-Record {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
>   no-eta-equality
>   constructor _,_
>   field
>     fst : A
>     snd : B fst
>
> open Σ-Record
>
> data Σ-Data {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
>   _,_ : (x : A) → B x → Σ-Data A B
>
> test-Record : {A : Set} {B : A → Set} → Σ-Record A B → Set
> test-Record product = let (a , b) = product in {!!}
>
> test-Data : {A : Set} {B : A → Set} → Σ-Data A B → Set
> test-Data product = let (a , b) = product in {!!} -- Error: Expected 
> record pattern
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161108/3dea5d74/attachment.html