coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Asking for simple example of advanced induction and recursion.
Date: Fri, 19 Jul 2013 14:51:24 +0300

For example, I have such Type:

Definition nzn: Type := {n: nat | n <> O}.

Can anyone write down all necessary theorems (with Admitted) and anything else that would allow use induction and recursion on that type?

[Coq-Club] Asking for simple example of advanced induction and recursion., Ilmārs Cīrulis, 07/19/2013
- Re: [Coq-Club] Asking for simple example of advanced induction and recursion., Rui Baptista, 07/21/2013