coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?

From: Thery Laurent <thery AT ns.di.univaq.it>
To: Milad Niqui <milad AT cs.kun.nl>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?
Date: Fri, 28 Nov 2003 11:56:20 +0100 (CET)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Fri, 28 Nov 2003, Milad Niqui wrote:

> Our canonical representation is essentialy like your original mkRat, we
> directly encode the unique proof of equlity (Zgcd m n)=1. So you can
> consider our representation to be:
>
> m/n -> (Zgcd m n)
>

Yes but yours does not extract in Ocaml is this true?

--
Laurent Thery

Re: [Coq-Club] Coq Poll: What are your preferred rational numbers ?, (continued)