Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Is Coq being too conservative?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is Coq being too conservative?


chronological Thread 
  • 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.



Archive powered by MhonArc 2.6.16.

Top of Page