The Coq mailing list

[jd AT sophia.inria.fr (Joelle Despeyroux)]

Dear all,

We used an axiom of extensionality in our experiments on formalizing
functional languages using the higher-order abstract syntax method 
in Coq, when formalizing the type Ln = L -> ... -> L -> L representing
the terms in L depending on n variables as 
(list L) -> L, with (list A) = nat -> A.

Using ordinary lists seemed just impossible.  Later on appeared the
possibility to define the above terms Ln using a fix point. 
Unfortunatly, we did not succeed in rewritting our specifications
using this nice type.

Joëlle Despeyroux and André Hirschowitz ,
Higher-order Syntax and Induction in Coq,
Fifth Int. Conf. on Logic Programming and Automated Reasoning, LPAR, 
Kiev, July 1994. Springer-Verlag LNAI 822. 

  Yours,
  Joelle Despeyroux