The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

What's the difference between 1st and 2nd example? The 2nd isn't accepted.

(* 1 *)

Require Import Utf8 List.

Set Implicit Arguments.

Inductive tree (A: Type) :=

 | leaf

 | root: list (tree A) → tree A.

Fixpoint count (T: tree nat) :=

  match T with

  | leaf _ => 1

  | root l => fold_right (λ x, plus (count x)) O l

  end.

 

(*2*)

Require Import Utf8.

Set Implicit Arguments.

Inductive list A: nat → Type :=

 | nil: list A 0

 | cons: ∀ n, A → list A n → list A (S n).

Inductive tree (A: Type) :=

 | leaf

 | root: ∀ n, list (tree A) n → tree A.

Fixpoint fold_right A B n (f: B → A → A) (a: A) (L: list B n): A :=

  match L with

  | nil _ => a

  | cons x t => f x (fold_right f a t)

  end.

Fixpoint count (T: tree nat) :=

  match T with

  | leaf _ => 1

  | root l => fold_right (λ x, plus (count x)) O l

  end.

(* Error:

Recursive definition of count is ill-formed.

In environment

count : tree nat → nat

T : tree nat

n : nat

l : list (tree nat) n

x : tree nat

Recursive call to count has principal argument equal to 

"x" instead of "l".

Recursive definition is:

"λ T : tree nat,

 match T with

 | leaf _ => 1

 | @root _ n l => fold_right (λ x : tree nat, Nat.add (count x)) 0 l

 end". *)