The Coq mailing list

[julien.forest AT ensiie.fr]

Hi Jonathan,

this is clearly a bug. Can you please fill a bug report and, if
possible, assign it to me 
(forest AT ensiie.fr).

The bug seems to come from the use of maximal implicit argument on Acc.
For now, you can then remove the brackets on Acc to recover a normal
behavior.

Best regard,
Julien



On Fri, 19 Sep 2014 15:56:55 -0400
Jonathan 
<jonikelee AT gmail.com>
 wrote:

> 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