The Coq mailing list

["Marcus Ramos" <mvmramos AT gmail.com>]

Hi,

As a novice user of Coq, I have difficulties deciding what is the best
definition for an inductive type. For example, I have this definition of a
string set:

Inductive string_set: Set :=
   | ss_empty: string_set
   | ss_str: string->string_set
   | ss_build: string_set->string_set->string_set.

which is appropriate for some purposes (a few fixpoints that I am writing).
However, for other purposes, I find it almost impossibile to advance with this
definition. In this case, the following definition suits better for my
objectives (another set of fixpoints):

Inductive string_set: Set :=
   | ss_empty: string_set
   | ss_str: string->string_set
   | ss_build: string->string_set->string_set.

(the difference is in the type of ss_build constructor).

My question is: how can I be able to take advantage of both ways of defining
this inductive type, and thus be able to define all my fixpoints properly? Can
I combine them somehow? Or convert from one to the other? Or...?

Thanks in advance,
Marcus.