The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 30 Apr 2008, Andrei Popescu wrote:

> I am trying to define a sum operator that takes a number n, a predicate P
> : Less n -> Prop,
> and a function f : {i : Less n | P i} -> nat, and returns the sum of all
> numbers f i such that
>  i : Less n and P i holds. 

I would recomment using a predicate P : Less n -> bool, which gives you 
the class of decidable predicates.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''