coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
- To: chris jhons <chrisformal AT yahoo.co.uk>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] even
- Date: Tue, 21 Sep 2004 19:15:04 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
The first function can be translated directly:
Fixpoint even (n:nat) : bool := match n with
| 0 => true
| 1 => false
| S (S n') => even n'
end.
One way to do cope with the mutual recursive definition is it to write both functions in one, and to define projections:
Fixpoint even'_odd (n:nat) : bool * bool :=
let even' i := fst (even'_odd i) in
let odd i := snd (even'_odd i) in
(match n with
| 0 => true
| S n => odd n
end,
match n with
| 0 => false
| S n => even' n
end).
Definition even' i := fst (even'_odd i).
Definition odd i := snd (even'_odd i).
(Of course this can be written somewhat shorter, but i'd like to suggest a more or less general scheme).
With lazy evaluation you can avoid caculating the values of both functions if you need just one.
Roland
- [Coq-Club] even, chris jhons
- Re: [Coq-Club] even, Roland Zumkeller
- Re: [Coq-Club] even,
Remi Vanicat
- Re: [Coq-Club] even, Roland Zumkeller
- Re: [Coq-Club] even,
Remi Vanicat
- Re: [Coq-Club] even, Roland Zumkeller
Archive powered by MhonArc 2.6.16.