coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Chris Dams <chris.dams.nl AT gmail.com>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] How to make mutual recursive theorems?
- Date: Tue, 2 Jun 2009 20:57:35 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=BPSFvggPqMmpYyMm8+35Q0Zj+idCJS1lZauyGM2szooY4CYUWCvk2QAXpMWhTZt329 nn5Mig9put58LKKvRH1+3i3z+NRA5IH1rw0HM2gMa9WMM/3HcUF79h2BciDgJJvmOZy9 HcSP8dsMffDg8b9xoRcA7m0tB+oSQ6QFFX8uE=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello Yves, Vincent and the rest of the list,
Yes, Scheme works, so thanks for that.
The Theorem ... with ... construction seems nice too and is a reason
to upgrade to 8.2, but does not work quite as well for me. If I do
Theorem mutual_ind_A:
forall P: A -> Prop,
forall Q: B -> Prop,
P mk_a ->
Q mk_b ->
(forall b: B, Q b -> P (S b)) ->
(forall a: A, P a -> Q (T a)) ->
forall a: A, P a
with mutual_ind_B:
forall P: A -> Prop,
forall Q: B -> Prop,
P mk_a ->
Q mk_b ->
(forall b: B, Q b -> P (S b)) ->
(forall a: A, P a -> Q (T a)) ->
forall b: B, Q b.
Coq answers with "Anomaly: uncaught exception Not_found. Please report."
All the best,
Chris
- Re: [Coq-Club] How to make mutual recursive theorems?, Chris Dams
- Re: [Coq-Club] How to make mutual recursive theorems?, Hugo Herbelin
Archive powered by MhonArc 2.6.16.