The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 31 Jan 2006, Carlos.SIMPSON wrote:

> Inductive FinConditional (n : nat) : bool -> Set :=
>  | fin_prev : FinConditional (pred n) (non_zero n) -> Fin n true
>  | fin_next : FinConditional n true.
>
> Definition Fin n := FinConditional n true.

I don't understand how this would be an improvement over either of my two
proposals.  Perhaps you could explain.

Also, Fin 0 ought to be empty, but this is (presumably) easy to fix.

-- 
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.''