Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is there a type representing the reals set (R) ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a type representing the reals set (R) ?


Chronological Thread 
  • From: "John Wiegley" <johnw AT newartisans.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Is there a type representing the reals set (R) ?
  • Date: Mon, 17 Nov 2014 16:28:51 -0600
  • Organization: New Artisans LLC

>>>>> CHAUVIN Barnabe
>>>>> <barnabe.chauvin AT gmail.com>
>>>>> writes:

> In Rdefinitions, I found the is_upper_bound definition, which represent the
> R set with the type R->Prop. It would be more understandable if it would be
> "Ensemble R", isn't it ? (This is the reason why I said I feel like the
> theories are not working together ..)

I've also found a few places where it seems that some parts of the stdlib
evolved separately from other parts, and at different times, so that they
express similar things in ways that are different enough to be cumbersome.

It might be nice to overhaul and create a stdlib v2, based on all the
experience gained thus far, using the most modern features of the upcoming Coq
8.5, and aiming at better consistency to a whatever core philosophy is chosen.

This is one reason why I've settled on ssreflect, and moved away from using
the stdlib, because they've definitely got the consistency going there.

John



Archive powered by MHonArc 2.6.18.

Top of Page