The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

In the following attempt to use Function to get a functional induction scheme:

Inductive btree : Set :=
| Leaf : btree
| Node : btree -> nat -> btree -> btree.

Function ascend{Acc : Set}
               (f : Acc -> nat -> Acc -> Acc)(i : Acc)
               (t : btree) {struct t}
         : Acc :=
  match t with
    | Leaf => i
    | Node lc a rc => f (ascend f i lc) a (ascend f i rc)
  end.

I get the warning "Cannot define graph(s) for ascend".  From the reference manual, this warning should occur if ascend uses pattern matching on dependent types, or if the definition is not a pattern-matching tree with applications only at the end of each branch.

To me, it looks like ascend is not violating either of those rules.  What am I missing here?

-- Jonathan