The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

You need to define:
Inductive term Set -> Set :=
  | Var : forall A:Set, A -> term A
  | App : forall A:Set, term A -> term A -> term A
  | Fun : forall A:Set, term (option A) -> term A.

Christine Paulin

roconnor AT theorem.ca
 writes:
 > Let me modify my previous question as follows.  Why must the parameters in
 > a parametric inductive definition be uniform?  For example, why should the
 > following declaration rejected:
 > 
 > Inductive term (A:Set) : Set :=
 >  | Var : A -> term A
 >  | App : term A -> term A -> term A
 >  | Fun : term (option A) -> term A.
 > 
 > The data type is still well-founded.  I would expect the generated
 > elimination rule to have a type such as:
 > 
 > term_rec : forall
 > (P:forall A:Set, term A -> Set)
 > (A:Set)
 > (var_case:forall a:A, P A (Var A a))
 > (app_case:forall a b:term A, P A a -> P A b -> P A (App A a b))
 > (fun_case:forall a:term (option A), P (option A) a -> P A (Fun A a))
 > (a:term A),
 > (P A a).
 > 
 > Would modifying Coq to allow non-uniform parametric inductive types lead
 > to an inconsistency or other badness?
 > 
 > -- 
 > Russell O'Connor                                      <http://r6.ca/>
 > ``All talk about `theft,''' the general counsel of the American Graphophone
 > Company wrote, ``is the merest claptrap, for there exists no property in
 > ideas musical, literary or artistic, except as defined by statute.''
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86