The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Ramana,

The usual way to do this kind of thing is to have term parametrized
by a typing context. Here is an example.

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

Inductive type : Set :=
  | base : type
  | arrow : type -> type -> type.

Definition Env := list type.

Inductive in_Env : type -> Env -> Set :=
  | here : forall s G, in_Env s (cons s G)
  | there : forall s t G, in_Env s G -> in_Env s (cons t G).

Inductive term (G : Env) : type -> Set :=
  | var : forall (s : type), in_Env s G -> term G s
  | lam : forall (s t : type), term (cons s G) t -> term G (arrow s t)
  | app : forall (s t : type), term G (arrow s t) -> term G s -> term G t.

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

Cheers,

--
guillaume



On 8 November 2011 17:36, Ramana Kumar 
<ramana.kumar AT gmail.com>
 wrote:
> Dear Coq Club
>
> I am writing my first (semi-)serious Coq file, and I'd like to get
> help from anyone willing to improve my style and tell me about things
> in the libraries I don't know about yet (and fix my errors...).
>
> I am trying to define the terms (and types) of simple type theory (aka
> higher-order logic) as an inductive datatype in Coq using dependent
> types to ensure that all terms are well-typed from the start. Is that
> possible?
>
> At the bottom of my file (attached) is the attempt to do it from the
> start. Above it, I also tried a more convoluted way where I first
> define preterms (which may not be well-typed) then try to take a
> subset of them. But I am running into problems with testing equality
> (among other things).
>
> A specific side-question: Is there a better way to get dependently
> typed lists than the way I have defined ilist?
> Any other comments on style are welcome.
>
> I look forward to any replies :)
>
> Thanks
> Ramana
>