coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fabrice Lemercier <nouvid-coq AT yahoo.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Exploiting variable binding of Coq for encoding lambda-calculus
- Date: Wed, 7 Dec 2005 06:30:29 +0100 (CET)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Message-ID:Received:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=EWmhessZp8MhDt+gjjPwT9y1PXcJVD/n/QZkevRjahh+qtR79HkVRAMq1znfkIkD2Vifvrnmujl3SVwEp17bU7R94yWZwsdvigta1W2acv8NLoxZ+kTcXrIEvRklF+FT5BpIpYTnAey26bKzTh1RpUDcGJMp9L6Lv5ZTB5hzUCQ= ;
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello
I want to encode lambda calculus is Coq in such a way that it uses the variable binding mechanism of Coq. But the following definition is rejected by Coq because of the non strictly positive occurrence of Term in (Term -> Term) -> Term.
Inductive Term : Set :=
abs : (Term -> Term) -> Term
| app : Term -> Term -> Term.
Is there a workaround?
Fabrice
Appel audio GRATUIT partout dans le monde avec le nouveau Yahoo! Messenger
Téléchargez le ici !
- [Coq-Club] Exploiting variable binding of Coq for encoding lambda-calculus, Fabrice Lemercier
Archive powered by MhonArc 2.6.16.