The Coq mailing list

["Jianzhou Zhao" <jianzhou AT seas.upenn.edu>]

Hey All,

 

I did some experiments of Coq's Function and Fixpoint,

and found Function with {measure ...} does not support the

syntax that Fixpoint can support.

 

////////////////////////////////////////

Require Import Arith.
Require Import Recdef.

 

Definition size (n:nat) := n.

 

Function test1 (n:nat) {struct n} : Prop :=
  match n with
  | O => True
  | S n' => forall (i:nat), test n'
  end
  .

Fixpoint test2 (n:nat) {struct n} : Prop :=
  match n with
  | O => True
  | S n' => forall (i:nat), test n'
  end
  .
Function test3 (n:nat) {measure size n} : Prop :=
  match n with
  | O => True
  | S n' => forall (i:nat), test n'
  end
  .

/////////////////////////////////////////////////

 

test1 and test2 work well. Coq reports 'User Error: find_call_occs : Prod'

for test3. But it does not give me any hint about the details of the user error.

And the Coq manual does not explain any limitation of Function with {measure ...}, either.

How can I fix this problem?

 

Thank you

Jianzhou