<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    It doesn't really matter, though, as Agda acknowledges that they are
    definitionally equal:<br>
    <br>
    ```<br>
    module LetPatterns where<br>
    <br>
    open import Data.Product<br>
    open import Relation.Binary.PropositionalEquality<br>
    <br>
    _∋_ : (A : Set) (a : A) → A<br>
    A ∋ a = a<br>
    <br>
    foo : ∀ {A : Set} {B : ∀ (a : A) → Set} → (p : Σ A B) → proj₁ p ≡
    proj₁ p<br>
    foo tup = let x , y = tup in (x ≡ proj₁ tup) ∋ refl<br>
    ```<br>
    <br>
    Andreas<br>
    <br>
    <div class="moz-cite-prefix">On 15/02/19 13:08, Guillaume Allais
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:7c75ee69-d4c6-f56a-4140-3d456a0f31c9@ens-lyon.org">
      <pre class="moz-quote-pre" wrap="">Hi,

This is a known problem (<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/1181">https://github.com/agda/agda/issues/1181</a>)
and unfortunately has not been fixed yet. It's in the 'icebox' meaning
that if anyone contributes a fix, it'll be gladly accepted but there
is no set deadline for it.

Cheers,
--
gallais

On 14/02/2019 23:28, Jason -Zhong Sheng- Hu wrote:
</pre>
      <blockquote type="cite">
        <pre class="moz-quote-pre" wrap="">Hi,

consider following program:

```
foo : ∀ {A : Set} {B : ∀ (a : A) → Set} → Σ A B → Set
foo tup = let x , y = tup in {!!}
```

In the hole there, we can see the following environment:

```
Goal: Set
————————————————————————————————————————————————————————————
y   : .B (proj₁ tup)
x   : .A
tup : Σ .A .B
.B  : .A → Set
.A  : Set
```

I think the highlighted part is quite unexpected, as I would consider let bindings have the same effect as with patterns when dealing with irrefutable patterns. In particular, I'd hope y has type `.B x` in this case. Is this a bug or expected behavior? I am asking this because it's quite confusing as it seems to indicate let bindings are very weak in agda.

Sincerely Yours,

Jason Hu


_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>

</pre>
      </blockquote>
      <pre class="moz-quote-pre" wrap="">
</pre>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>