coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Adding strong induction to the standard library
Date: Mon, 5 Dec 2016 10:30:55 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f181.google.com
Ironport-phdr: 9a23:/y85chUZvtuoKzhmmTT+4iTeMp3V8LGtZVwlr6E/grcLSJyIuqrYZRKDt8tkgFKBZ4jH8fUM07OQ6PG7HzBQqszc+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga5tzKg+3pEPfrJo4m4xnf5o8yFPionJKdugekX9jJVuRkhrU48asupNv7nID6Loa68dcXPCiLOwDRrtCAWF+Pg==

The standard library does not include strong induction. Could it be added? A proposed addition is at https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v. Comments welcome, including nitpicks on the comments and pull requests.

Thanks!

Tej

[Coq-Club] Adding strong induction to the standard library, Tej Chajed, 12/05/2016
- Re: [Coq-Club] Adding strong induction to the standard library, Robbert Krebbers, 12/05/2016
- Re: [Coq-Club] Adding strong induction to the standard library, Dominique Larchey-Wendling, 12/05/2016
  - Re: [Coq-Club] Adding strong induction to the standard library, Tej Chajed, 12/05/2016
    - Re: [Coq-Club] Adding strong induction to the standard library, Dominique Larchey-Wendling, 12/05/2016