coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A new member

From: "X.X.X. " <rabudo AT mixmail.com>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Cc: "brais AT lycos.com" <brais AT lycos.com>
Subject: [Coq-Club] A new member
Date: Thu, 17 Jan 2002 13:17:37 +0100
Xmailer: Mixmail Server 2.0

HI! My name is Joao I'm a new member of the Coq Club. I would like to know how to define new operations using the recursive scheme _rec I. e. If I have the next definition: Coq < Inductive list [X:Set]:Set := Coq < Nil : (list X) Coq < | Cons: X -> (list X) -> (list X). list_ind is defined list_rec is defined list_rect is defined list is defined How I could define a function that concatenate two lists using list_rec? Thanks Joao

Tu correo gratis en MixMail
Ya.com ADSL. Módem + Alta gratis

[Coq-Club] A new member, X.X.X.
- Re: [Coq-Club] A new member, Jean-Christophe Filliatre
- Re: [Coq-Club] A new member, Christine Paulin