<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta content="text/html; charset=utf-8">
</head>
<body bgcolor="#FFFFFF">
<div dir="auto">That's because product itself having definitional eta expansion, isn't it? What about those having not? Let me try later.<br>
<br>
<div>Thanks,<br>
Jason Hu</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Feb 15, 2019 08:24, Andreas Nuyts <andreas.nuyts@cs.kuleuven.be> wrote:<br type="attribution">
</div>
</div>
<div>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">
<pre class="moz-quote-pre">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">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">
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre">_______________________________________________
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>
</div>
</body>
</html>