The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Eugene Kirpichov wrote:
> Inductive btree (t:Set) :=
>   | BLeaf : t ->  btree t
>   | BNode : btree t ->  btree t ->  btree t.
>
> Inductive trexp : Set :=
>   | TLeaf : nat ->  trexp
>   | TNode : btree trexp ->  trexp.
>
> Fixpoint total (t:trexp) :=
>   match t with
>   | TLeaf n =>  n
>   | TNode b =>  btotal b
>   end
> with btotal (b:btree trexp) :=
>   match b with
>   | BLeaf t =>  total t (* An error here? *)
>   | BNode b1 b2 =>  btotal b1 + btotal b2
>   end.
>
> I get the following error...
>    

This program is rejected for the same reason that the first version of 
[nat_tree_ind'] is rejected in the chapter where you got the exercise 
(on page 55).  Recursion over nested inductive types needs to be 
implemented with nested recursion, not mutual recursion.  It's a 
hard-coded restriction; I'm not aware of any intuition behind it.