The Coq mailing list

[Colm Bhandal <bhandalc AT tcd.ie>]

If you want a set containing nats and bools you could just use the disjoint union:

Open Scope type_scope.

Definition natBool := nat + bool.

Alternatively you could, as Kris said, use your own constructors for more clarity:

Inductive natBool :=
  | nbNat : nat -> natBool
  | nbBool : bool -> natBool.

The latter way is probably preferable since the tags themselves are indicative of the raw underlying value, whereas in the disjoint union type, the tags are just "inl" and "inr".

Then if you want a list of these natBools, the type is simply:

Definition listNatBool := list natBool.

Another alternative is to construct a new type of list with two concatenation constructors:

Inductive listNatBool :=
  | nil : listNatBool
  | constNat : nat -> listNatBool -> listNatBool
  | constBool : bool -> listNatBool -> listNatBool.

On 26 February 2013 16:41, Kristopher Micinski <krismicinski AT gmail.com> wrote:

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?