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