The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Amelia Viorela Rastei wrote:
>    How can I define the set of terms of the syntax:
> 
>    T ::= S | VAR | Pi VAR : T.T | Lambda VAR : T.T | TT
> 
>   lets say S={s,t}
>   so I would be able to have a variable ranging over this type.

Hello,

Seems like you are interested in formalising the Calculus of
Constructions or something similar!
A few years ago, I wrote a contribution (called coq-in-coq) that
formalises many aspects of the metatheory of CC: confluence, subject
reduction, strong normalisation, decidability of type-checking.
I suggest you have a look at
http://coq.inria.fr/~barras/rr/index-eng.html
and more specifically http://coq.inria.fr/~barras/rr/Termes.html where
the set of terms and substitution is defined. It uses de Bruijn indices
for variables, that's why Pi and Lambda do not have names attached to
them.

A version of the contribution is available from
http://coq.inria.fr/contribs-eng.html
If you have the last version of Coq (V7.2):
http://coq.inria.fr/contributions/V7.2/coq-in-coq.tar.gz

Hope it helps,

Bruno Barras.

-- 
  Projet LogiCal - INRIA Rocquencourt
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://logical.inria.fr/~barras
-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/