coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Function {measure}" and induction principles

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: AUGER Cedric <Cedric.Auger AT lri.fr>
Cc: Chris Casinghino <chris.casinghino AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Function {measure}" and induction principles
Date: Wed, 29 Jun 2011 11:58:56 +0200

Hello Cedric,

I get the error

"Error: Nested recursive function are not allowed with Function"

this is indeed a nested recursive call since dummy_trick is not
unfolded. Nested recursive calls are currently not in the scope of
Function.

Bests,
Pierre

2011/6/29 AUGER Cedric
<Cedric.Auger AT lri.fr>:
> (* By the way, I get some very unexpected error if I replace
> � the critical part with :
> � � "let H: Foo := go_right3 f1 in
> � � �go_right3 (dummy_trick H f2)" *)

[Coq-Club] "Function {measure}" and induction principles, Chris Casinghino
- Re: [Coq-Club] "Function {measure}" and induction principles, AUGER Cedric
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
- Re: [Coq-Club] "Function {measure}" and induction principles, David Pichardie
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
    - Re: [Coq-Club] "Function {measure}" and induction principles, Chris Casinghino