The Coq mailing list

[Satrajit Roy <admin AT satrajit.com>]

I'm new to Coq. How can I define something like the following in Coq:
  
  Inductive kind:Set:= | x | y | z.
  
  Inductive xKind:kind:=|x'|x''|..|x''''.
  Inductive yKind:kind:=|y'|y''|..|y''''.
  Inductive zKind:kind:=|z'|z''|..|z''''.
  
  FixPoint funcKind (k:kind) (...) .. {struct k} : kind := match k with
  | x => some recursive term using xKind
  | y => some recursive term using yKind
  | z => some recursive term using zKind
  end.
  
  I know the above is syntactically wrong. But I hope I got my intention across.
  Is the above even possible?
  
  Thanks in anticipation.