The Coq mailing list

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

Hello all,

I am trying to further develop the library String, and thus have the following
piece of code:

Inductive string: Set :=
   | epsilon: string
   | sym: ascii->string
   | cat: ascii->string->string.

Fixpoint append (s1 s2: string): string :=
   match s1 with
   | epsilon => s2
   | sym c => cat c s2
   | cat c s => cat c (append s s2)
   end.

I would like to write a fixpoint stringdenote that parses, for example:

(cat "a" (sym "b"))(sym "c")

and returns "abc" in the screen. Does any one know I can achieve this? In
other words, how can I build a string of characters as a return value of this
fixpoint and print the value on the screen? Sorry if this is too basic, but I
really haven´t found my way through.

Thanks in advance,
Marcus.