<div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hi Gergo,<div> So the first thing to say is that due to an oversight, the functionality of `All<span style="color:rgb(80,0,80);font-size:12.8px">₂` </span><span style="font-size:12.8px"><font color="#000000">in</font></span><span style="color:rgb(80,0,80);font-size:12.8px"> </span>`Data.Vec.All` is actually a duplicate of the existing datatype `Relation.Binary.Vec.<wbr>Pointwise`. In the upcoming release of the library at the end of January, we're deprecating `All<span style="font-size:12.8px"><font color="#000000">₂` and moving `Relation.Binary.Vec.<wbr>Pointwise` to `Data.Vec.Relation.<wbr>InductivePointwise` and `Data.Vec.Relation.<wbr>ExtensionalPointwise`. Feel free to have a look at the CHANGELOG in <a href="https://github.com/agda/agda-stdlib/tree/master/src" target="_blank">standard library</a> repository for a more detailed explanation.</font></span></div><div><span style="font-size:12.8px"><font color="#000000"><br></font></span></div><div><span style="font-size:12.8px"><font color="#000000">That's not to say your proofs wouldn't be a welcome contribution to the library! The natural place for it in v0.15 will be in the new module `Data.Vec.Relation.<wbr>InductivePointwise`. I would probably name them something like </font></span><span style="font-size:12.8px"><font color="#000000">`</font></span><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">pointwise</font></span><font color="#000000" face="SFMono-Regular, Consolas, Liberation Mono, Menlo, Courier, monospace"><span style="font-size:12px;white-space:pre-wrap">ˡ</span></font><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">⇒</font></span><span style="color:rgb(0,0,0);font-size:12.8px">all</span><font color="#000000" face="SFMono-Regular, Consolas, Liberation Mono, Menlo, Courier, monospace"><span style="font-size:12px;white-space:pre-wrap">` and `</span></font><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">pointwise</font></span><span style="color:rgb(111,66,193);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">ʳ</span><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">⇒</font></span><span style="color:rgb(0,0,0);font-size:12.8px">all</span><font color="#000000" face="SFMono-Regular, Consolas, Liberation Mono, Menlo, Courier, monospace"><span style="font-size:12px;white-space:pre-wrap">`</span></font><span style="font-size:12.8px"><font color="#000000">, and possibly add their counterparts `all</font></span><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">⇒pointwise</font></span><font color="#000000" face="SFMono-Regular, Consolas, Liberation Mono, Menlo, Courier, monospace"><span style="font-size:12px;white-space:pre-wrap">ˡ` and `</span></font><span style="font-size:12.8px"><font color="#000000">all</font></span><span style="font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap"><font color="#000000">⇒pointwise</font></span><span style="color:rgb(111,66,193);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:12px;white-space:pre-wrap">ʳ</span><font color="#000000" face="SFMono-Regular, Consolas, Liberation Mono, Menlo, Courier, monospace"><span style="font-size:12px;white-space:pre-wrap">`</span></font><span style="font-size:12px;white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, helvetica, sans-serif"> as well</font></span><span style="font-size:12px;white-space:pre-wrap;color:rgb(0,0,0);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace">.</span><span style="font-size:12px;white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, helvetica, sans-serif"> If you'd like to add them, feel free to submit a pull request to the library and they can be added to the upcoming release.</font></span></div><div><span style="font-size:12.8px"><font color="#000000"><br></font></span></div><div><span style="font-size:12.8px"><font color="#000000">Thanks,</font></span></div><div><span style="font-size:12.8px"><font color="#000000">Matthew</font></span></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Sat, Jan 6, 2018 at 6:26 AM, Dr. ERDI Gergo <span dir="ltr"><<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><span>On Sat, 6 Jan 2018, Dr. ERDI Gergo wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
all₂₁ : ∀ {a b} {A : Set a} {B : Set b} {P : A → Set}<br>
 {n} {xs : Vec A n} {ys : Vec B n} →<br>
 All₂ (λ x y → P x) xs ys → All P xs<br>
all₂₁ []        = []<br>
all₂₁ (p ∷ ps)  = p ∷ all₂₁ ps<br>
</blockquote>
<br></span>
Of course there's a symmetric all₂₂ with (λ x y → P y)as well.<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</div><br></div>