[Agda] recursive \times

[Andreas Abel]

A list of types is not a type.

On 12.04.13 12:51 PM, Dr. ÉRDI Gergő wrote:
> Look at Data.List.All in the std lib.
>
> On Apr 12, 2013 6:48 PM, "Serge D. Mechveliani" <mechvel at botik.ru
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/