coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Definitions using well-founded arguments

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: alexander AT math.ohio-state.edu
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Definitions using well-founded arguments
Date: Sat, 19 Nov 2011 06:02:55 +0100

Hi,

On Sat, Nov 19, 2011 at 5:18 AM,
<alexander AT math.ohio-state.edu>
wrote:
> Program Fixpoint InterpretTerm (T : Term) (s : Assignment) : nat { measure
> (TermDepth T) } :=

the measure needs to be given just before the : for the return type:

Program Fixpoint InterpretTerm (T : Term) (s : Assignment) { measure
(TermDepth T) }: nat :=

Cheers

[Coq-Club] Definitions using well-founded arguments, alexander
- Re: [Coq-Club] Definitions using well-founded arguments, Alexandre Pilkiewicz