The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Perhaps you should read some introductory Coq material.

http://www.labri.fr/perso/casteran/RecTutorial.pdf

It could be as simple as (depending on what you want) defining an
inductive type with two cases, a nat or bool (if you mean bool in the
Set sense..)

Kris

On Tue, Feb 26, 2013 at 11:34 AM, fengsheng 
<fsheng1990 AT 163.com>
 wrote:
> Hello everyone !
>   I want to define a new type which is available for nat and bool,but I 
> could
> not to work out it.I mean it is just a list including nat and bool.How to
> define this new type?