coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] syntactical conditions for generation of functional schemes

From: Max Schaefer <xiemaisi AT yahoo.de>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] syntactical conditions for generation of functional schemes
Date: Tue, 8 Apr 2008 00:58:28 -0700 (PDT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.de; h=X-YMail-OSG:Received:Date:From:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=Jmy7dI0dWoAgKb8J7aU4+lsM04ednOeLLELyTM49qLsc94Lti3kfxWeroxHhC+SHUUK9ATQQ5nOIILDMKIlIi5Mvh1chCqy00YsLN2jBLP+45zTeXjEVjwI3C0+OEDMhLSTYZF0tnL8lHQv3dRcu26Vi2wBj/4Xje3TJpmeTSHc=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

I've been trying to use functional induction recently,
and while it's really great when it works, it often
doesn't because the Functional Scheme command fails.

Now the manual gives some hints at the syntactic
requirements a function must fulfill in order for an
induction scheme to be generated (rigid arguments
first, "match tree" structure), but it is a bit vague.
Is there a more precise reference available somewhere?

Cheers,

-- Max

____________________________________________________________________________________
You rock. That's why Blockbuster's offering you one month of Blockbuster
Total Access, No Cost.
http://tc.deals.yahoo.com/tc/blockbuster/text5.com

[Coq-Club] syntactical conditions for generation of functional schemes, Max Schaefer