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

[Andreas Abel]

See https://github.com/agda/agda/issues/2298 for why a language change 
is unlikely to happen.

On 08.11.2016 23:57, Martin Stone Davis wrote:
> 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
>>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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