The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

Hello,

There is different ways in Coq for defining such a function. One is to
use the 'Function' definition:

Require Import ZArith.
Require Import Recdef.
Open Scope Z_scope.

Function SumFilterZRec (z: Z) (filter: Z -> bool) (hi: Z) {wf Zgt z} :
Z :=
   match Zcompare z hi with
   | Lt => if filter z then
             z + SumFilterZRec (Zsucc z) filter hi
           else
             SumFilterZRec (Zsucc z) filter hi
   | _ => 0
   end.

Definition SumFilterZ (filter : Z -> bool) (lo : Z) (hi : Z) : Z :=
   match Zcompare lo hi with
   | Lt => SumFilterZRec lo filter hi
   | _ => 0
   end.


-- 
Jean-Marc Notin
LIX - Équipe TypiCal

Attachment: smime.p7s
Description: S/MIME cryptographic signature