[Agda] recursive \times

[Dr. ÉRDI Gergő]

Look at Data.List.All in the std lib.
On Apr 12, 2013 6:48 PM, "Serge D. Mechveliani" <mechvel at botik.ru> wrote:

> Please, why the program below is not type-checked?
>
>   EachPositive : List Nat -> List (Set _)
>   EachPositive xs =  map (\ n -> n > 0) xs
>
>   f : (ns : List Nat) -> EachPositive ns -> Nat
>   f _ _ = 0
>
> -- a contrived example:  f takes  ns  and needs to use a proof for n > 0
> for each  n  in  ns.
>
> If I comment out  f,  then  EachPositive  is compiled
> (despite that I expected   "List (Set _)"  to be wrong).
>
> What should be the intended signature for  f  ?
>
> I attach to this letter     t.agda.zip
>
> -- the variant with  ManyProduct  -- with applies \times  recursively.
>
> 1) Has Standard library something close to  ManyProduct ?
> 2) Can the attempt with  map (\ n -> n > 0)  be improved, or it is just a
>    basically wrong idea?
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130412/1ee0dbd4/attachment.html