The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

Dear Marino,

Unfortunately, there is no written formal description of the
modifications introduced in the guardedness condition, but you will
find an illustrative example at the end of this mail.  There were no
modifications to cofixpoint definitions.

Coq's code evolves faster than we write new versions of the manual, so
it's very likely that the current manual is outdated.

Cheers,
Eduardo Gimenez.

PS: Here there is a simple example of what can be done now:
Require PolyList.
Implicit Arguments On.
Inductive list [A:Set] : Set := nil : (list A) | cons : A->(list A)->(list A).
Inductive Set Tree := Node : (list Tree) -> Tree.

Section Toto.
Variables A,B : Set.
Variable  h   : A->B->B.
Variable  b   : B.
Fixpoint ffold [l:(list A)] : B := 
  Case l of 
    b 
   [a:A][l1:(list A)](h a (ffold l1))
  end.
Variable  f   : A->B.
Fixpoint mmap [l:(list A)] : (list B) := 
  Cases l of 
    nil => (nil B) 
|   (cons a l1) => (cons (f a) (mmap l1))
  end.
End Toto.

Fixpoint sum [t:Tree] : nat := 
  Cases t of 
   (Node l) => (ffold [a:Tree][n:nat](plus (sum a) n) O l)
  end.