Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Lists of Multiple Types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lists of Multiple Types


Chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: mcano.programas AT gmail.com
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Lists of Multiple Types
  • Date: Sun, 10 Mar 2013 08:04:57 +0100

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.






Archive powered by MHonArc 2.6.18.

Top of Page