The Coq mailing list

[t x <txrev319 AT gmail.com>]

I recommend using something like:

(* note, following code not tested *)

Require Import List.

Definition string_set := list string.

Function ss_cons (s: string) (lst: list string) := a :: lst.

Function ss_union (s1: list string) (s2: list string) := s1 ++ s2.

On Sun, Jul 21, 2013 at 2:56 PM, Marcus Ramos <mvmramos AT gmail.com> wrote:

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.