<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p>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.)</p>
<p>To make it more convenient to use 'let' on product types, I
issued a <a
href="https://github.com/UlfNorell/agda-prelude/pull/45">pull
request on the agda-prelude</a>, changing Σ from data to record.
I would have preferred to leave agda-prelude as-is if 'let' could
be enhanced.<br>
</p>
<blockquote type="cite">
<p>open import Agda.Primitive<br>
<br>
infixr 1 _,_<br>
record Σ-Record {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b)
where<br>
no-eta-equality<br>
constructor _,_<br>
field<br>
fst : A<br>
snd : B fst<br>
<br>
open Σ-Record<br>
<br>
data Σ-Data {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b)
where<br>
_,_ : (x : A) → B x → Σ-Data A B<br>
<br>
test-Record : {A : Set} {B : A → Set} → Σ-Record A B → Set<br>
test-Record product = let (a , b) = product in {!!}<br>
<br>
test-Data : {A : Set} {B : A → Set} → Σ-Data A B → Set<br>
test-Data product = let (a , b) = product in {!!} -- Error:
Expected record pattern<br>
</p>
<p></p>
</blockquote>
<br>
</body>
</html>