The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  I think that this question was asked (and answered) a few days ago  
in the list.

There are (at least) two simple answers :

either use the List library (and all its theoremes and functions on lists)
on a type of the form (A+B),

or directly define your type with three constructors :
empty list, add a value of type A, and add a value of type B.


Pierre

Require Import List.

Definition nb: Type  := (nat+bool)%type.

Definition mixed_list := list nb.

Fixpoint number_of_nats (l :mixed_list) : nat :=
match l with nil => 0
           | inl _ :: l' => 1+ number_of_nats l'
           | inr _ :: l' => number_of_nats l'
end.

Compute number_of_nats (rev (inl 6 ::  inr true :: inl 7 :: inr false  
:: nil)).

Inductive mlist : Type :=
| mnil
| ncons : nat -> mlist -> mlist
| bcons : bool -> mlist -> mlist.

Check (ncons 6 (bcons true (ncons 8 mnil))).

Fixpoint number_of_nats' (m:mlist) : nat :=
match m with mnil => 0
           | ncons _ m' => 1 + number_of_nats' m'
           | bcons _ m' => number_of_nats' m'
end.




Quoting 
mcano.programas AT gmail.com:

> Good Night,
>
> I'm pretty new to coq and all the logic beneath it, but i was wondering if it
> is possible to define a collection of things with different types, the thing
> if i have two inductive definitions and i need a list that can contain types
> of the two definitions, is this possible, maybe can anyone give me an example
> on how to do it?
>
> Thank you all beforehand.