coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeff Terrell <jeff AT kc.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Is Coq being too conservative?
- Date: Wed, 20 Jan 2010 13:12:30 +0000
Hi,
Is Coq being too conservative in rejecting the definition of f?
Require Import List.
CoInductive A : Set :=
Build_A : list B -> A
with B : Set :=
Build_B : A -> B.
Definition RB := fun a : A => let (RB) := a in RB.
Definition RA := fun b : B => let (RA) := b in RA.
CoInductive X : Set :=
Build_X : list Y -> X
with Y : Set :=
Build_Y : X -> Y.
CoFixpoint f(a : A) : X :=
Build_X (map g (RB a))
with g (b : B) : Y :=
Build_Y (f (RA b)).
Thanks.
Regards,
Jeff.
- [Coq-Club] Is Coq being too conservative?, Jeff Terrell
- Re: [Coq-Club] Is Coq being too conservative?, AUGER
- Message not available
- Re: [Type-Based Guardednees Checking] Re: [Coq-Club] Is Coq being too conservative?,
Jeff Terrell
- Message not available
- Re: [Coq-Club] Is Coq being too conservative?, Chris Dams
- Re: [Type-Based Guardednees Checking] Re: [Coq-Club] Is Coq being too conservative?, Adam Chlipala
- Message not available
- Re: [Type-Based Guardednees Checking] Re: [Coq-Club] Is Coq being too conservative?,
Jeff Terrell
Archive powered by MhonArc 2.6.16.