[Agda] recursive \times
Serge D. Mechveliani
mechvel at botik.ru
Fri Apr 12 12:47:26 CEST 2013
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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 543 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130412/c682fa17/t.agda.zip
More information about the Agda