coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Is there a type representing the reals set (R) ?, CHAUVIN Barnabe, 11/17/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, John Wiegley, 11/17/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, Daniel Schepler, 11/17/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, CHAUVIN Barnabe, 11/18/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, Daniel Schepler, 11/18/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, CHAUVIN Barnabe, 11/18/2014
Archive powered by MHonArc 2.6.18.