The Coq mailing list

[jean-francois.monin AT imag.fr]

Hello, 

If you mean "some recursive term of type xKind" etc. instead of
"some recursive term using xKind", yes. 
This is not inheritance but dependent types.

You need a function such as
Definition kind_of k := 
  match k with
   | x => xKind
   | y => yKind
   | z => zKind
 end.

Then the body of your fixpoint is something like this:

 match k return kind_of k with
   | x => something of type xKind
   | y => something of type yKind
   | z => something of type zKind
 end.

Hope this helps,
  JF
    
Satrajit Roy a ecrit :
 > 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.

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 03 72
F-38610 GIERES                fax (+33 | 0) 4 56 52 03 44