The Coq mailing list

[richard dapoigny <richard.dapoigny AT univ-smb.fr>]

Dear all,

I read in the Coq doc that inductive types may admit coercions within their constructor (see https://coq.inria.fr/refman/Reference-Manual021.html#sec657).

However, when I try it, i get an error:
Error: The type of constructor es is not valid; it must be "EpsilonStarL" applied to its parameters.

I forward the code below.
Thanks for your help.
Richard

=========================================

Inductive Name : Type :=
  | bottom        : Name
  | top              : Name
  | name         : Name
  | unaryF       : Name -> Name
  | binaryF      : Name -> Name -> Name
  | ternaryF     : Name -> Name -> Name -> Name.

Inductive NS : Type := ns : NS.
Inductive NP : Type := np : NP.
Inductive NE : Type := ne : NE.

Variable cs  : NS -> Name.
Variable cp  : NP -> Name.
Variable ce  : NE -> Name.

Coercion cs  : NS >-> Name.
Coercion cp  : NP >-> Name.
Coercion ce  : NE >-> Name.

Definition star (a:Name)(A:NS) := binaryF a A.

Inductive Epsilon (A :NS) (b:Name) : Prop :=  epsilon : Epsilon A b.

Inductive EpsilonStarL (A B:NS) (b:Name) : Prop := es :> Epsilon A (star b B).