The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

It is surprising to me that in the fixpoint below, Coq cannot figure out that `children` is

a subterm of nodes. Theoretically, it seems that as long as a term is produced by peeling off one or more constructors (and doing nothing else), it should be considered a subterm. Are there some soundness or practicality issues in supporting such fixpoints?

Meanwhile, is there a way to write the fixpoint below without complicating the definition too much?

Require Import Coq.Lists.List.
Import ListNotations.

Inductive tree :=
| node (data: bool) (children: list tree).

Fixpoint nodesWithCont (nodes: list tree): list (tree* list tree) :=
   match nodes with
   | [] => []
   | (node d children)::tl =>  [(node d children, tl)] ++ (nodesWithCont children)++
                                                       nodesWithCont tl
   end.

Error: Recursive call to nodesWithCont has principal argument equal to "children" instead of

"tl".

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/