The Coq mailing list

[Eugene Kirpichov <ekirpichov AT gmail.com>]

2010/1/23 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.
>

Oh yes, indeed, thanks! By the time I solved the preceding exercises I
already forgot about that part of text :-|

-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru