The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 9 Mar 2005, Christine Paulin wrote:

>
> 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

This, of course, requires impredicate set. :-/

Also by this arguement we ought to get rid of parametric types entirely
and simplify the whole system.

-- 
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.''