<p>Look at Data.List.All in the std lib.</p>
<div class="gmail_quote">On Apr 12, 2013 6:48 PM, &quot;Serge D. Mechveliani&quot; &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Please, why the program below is not type-checked?<br>
<br>
  EachPositive : List Nat -&gt; List (Set _)<br>
  EachPositive xs =  map (\ n -&gt; n &gt; 0) xs<br>
<br>
  f : (ns : List Nat) -&gt; EachPositive ns -&gt; Nat<br>
  f _ _ = 0<br>
<br>
-- a contrived example:  f takes  ns  and needs to use a proof for n &gt; 0<br>
for each  n  in  ns.<br>
<br>
If I comment out  f,  then  EachPositive  is compiled<br>
(despite that I expected   &quot;List (Set _)&quot;  to be wrong).<br>
<br>
What should be the intended signature for  f  ?<br>
<br>
I attach to this letter     t.agda.zip<br>
<br>
-- the variant with  ManyProduct  -- with applies \times  recursively.<br>
<br>
1) Has Standard library something close to  ManyProduct ?<br>
2) Can the attempt with  map (\ n -&gt; n &gt; 0)  be improved, or it is just a<br>
   basically wrong idea?<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div>