Thanks Pierre. Appreciate it.
Sunil
________________________________________
From:
pierre.courtieu@... [
pierre.courtieu@...] On Behalf Of Pierre Courtieu [
Pierre.Courtieu@...]
Sent: Wednesday, October 21, 2009 3:29 AM
To: Sunil Kothari
Cc:
coq-club@...
Subject: Re: [Coq-Club] Functional Induction tactic being experimental
Function and functional induction are marked as experimental because it may be reimplemented in the next two years. However its semantic should not change much in the case that it already deals with. In this sense we could have removed the word "experimental" from the documentation. You can use it with no worry. I encourage you to do so and to report bugs/needs.
However this feature has some limitations, mainly on dependently typed functions, that we hope to work on during the next months/years. In this sense this feature is still in development.
Hope this helps,
Pierre Courtieu
2009/10/20 Sunil Kothari <
skothari@...<mailto:
skothari@...>>
Hi,
Could some one explain why the Coq manual (v 8.2 and earlier) describes the functional induction tactic as "experimental" ? I would appreciate any papers/pointers at the issues involved in using this tactic.
Thanks,
Sunil
--------------------------------------------------------
Bug reports:
http://logical.saclay.inria.fr/coq-bugsArchives:
http://pauillac.inria.fr/pipermail/coq-club http://pauillac.inria.fr/bin/wilma/coq-clubInfo:
http://pauillac.inria.fr/mailman/listinfo/coq-club--------------------------------------------------------
Bug reports:
http://logical.saclay.inria.fr/coq-bugsArchives:
http://pauillac.inria.fr/pipermail/coq-club http://pauillac.inria.fr/bin/wilma/coq-clubInfo:
http://pauillac.inria.fr/mailman/listinfo/coq-club
