coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Finite Types: Sorry a little modif!

From: "Carlos.SIMPSON" <carlos AT math.unice.fr>
To: roconnor AT theorem.ca
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club]Finite Types: Sorry a little modif!
Date: Tue, 31 Jan 2006 10:24:46 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Sorry about this but the definition in the previous message wasn't right: this should be better
and also it no longer needs boolset:

Definition non_zero (n:nat) : bool :=
match n with 0 => false | S m => true end.

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.

[Coq-Club]Proposal for Finite Types in the Standard Library, roconnor
- Re: [Coq-Club]Proposal for Finite Types in the Standard Library, Carlos.SIMPSON
- Re: [Coq-Club]Finite Types: Sorry a little modif!, Carlos.SIMPSON
  - Re: [Coq-Club]Finite Types: Sorry a little modif!, roconnor