<p>Look at Data.List.All in the std lib.</p>
<div class="gmail_quote">On Apr 12, 2013 6:48 PM, "Serge D. Mechveliani" <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> 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 -> List (Set _)<br>
EachPositive xs = map (\ n -> n > 0) xs<br>
<br>
f : (ns : List Nat) -> EachPositive ns -> Nat<br>
f _ _ = 0<br>
<br>
-- a contrived example: f takes ns and needs to use a proof for n > 0<br>
for each n in ns.<br>
<br>
If I comment out f, then EachPositive is compiled<br>
(despite that I expected "List (Set _)" 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 -> n > 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>