coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Lists of Multiple Types, mcano.programas, 03/10/2013
- Re: [Coq-Club] Lists of Multiple Types, Pierre Casteran, 03/10/2013
- Re: [Coq-Club] Lists of Multiple Types, Paolo Herms, 03/10/2013
- Re: [Coq-Club] Lists of Multiple Types, Paolo Herms, 03/10/2013
Archive powered by MHonArc 2.6.18.