[Agda] list of types

[Andreas Abel]

On 15.04.2013 11:44, Serge D. Mechveliani wrote:
> Andreas Abel responded recently
>
>> A list of types is not a type.
>
> But why
>         EachPositive : List Nat -> List (Set _)
>         EachPositive xs =  map (\ n -> n > 0) xs
>
> is type-checked?

This is fine, "List Set" is a type, but "EachPositive xs" is a list, and 
cannot be used as a type, as in,

   -> EachPositive xs -> ...




-- 
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/