Stream: math-comp analysis

Topic: boolp

Pierre-Yves Strub (Feb 17 2022 at 13:57):

Hi. What is the status of boolp?

Pierre-Yves Strub (Feb 17 2022 at 13:57):

If this module is still live, should it be factored out of mathcomp-analysis?

Pierre-Yves Strub (Feb 17 2022 at 13:57):

(I might need it in some dev.)

Cyril Cohen (Feb 17 2022 at 14:00):

It is live, and where would you want it to be factored out?

Cyril Cohen (Feb 17 2022 at 14:00):

a new classical-mathcomp repo or something?

Pierre-Yves Strub (Feb 17 2022 at 14:00):

I don't know, but pulling mathcomp-analysis just to have Prop = bool seems a bit violent ;)

Cyril Cohen (Feb 17 2022 at 14:00):

We should do some cleaning in it though...

Cyril Cohen (Feb 17 2022 at 14:01):

Pierre-Yves Strub said:

I don't know, but pulling mathcomp-analysis just to have Prop = bool seems a bit violent ;)

Sure, that's true... but making a one file package also seems weird (although we have bigenough in this case already)

Cyril Cohen (Feb 17 2022 at 14:01):

But maybe the classical sets and functions would make sense as part of this lib?

Pierre-Yves Strub (Feb 17 2022 at 14:02):

Cyril Cohen said:

But maybe the classical sets and functions would make sense as part of this lib?

Certainly

Cyril Cohen (Feb 17 2022 at 14:02):

Or more generally general bridges between mathcomp and bool = Prop, right?

Cyril Cohen (Feb 17 2022 at 14:02):

(but no topological spaces etc)

Cyril Cohen (Feb 17 2022 at 14:02):

Would make sense as it is getting more and more stable...

Pierre-Yves Strub (Feb 17 2022 at 14:03):

Yup. Meanwhile, I'm just going to copy this file.

Reynald Affeldt (Feb 17 2022 at 14:21):

Pierre-Yves Strub said:

Hi. What is the status of boolp?

During the last meeting, we actually discussed some of its contents (we removed some commented code), we realized that it is one of the files that crucially lacks documentation (and I was supposed to do something), and the soon-to-be-merged Lebesgue measure/integral branch is actually adding some useful things to it.

Reynald Affeldt (Feb 17 2022 at 14:25):

Cyril Cohen said:

But maybe the classical sets and functions would make sense as part of this lib?

Especially classical sets I think, don't they provide a significant improvement over the Ensembles from the standard library?

Reynald Affeldt (Feb 25 2022 at 00:56):

@Pierre-Yves Strub Would this issue answer your need? https://github.com/math-comp/analysis/issues/550

Pierre-Yves Strub (Feb 25 2022 at 07:45):

Yep.

Reynald Affeldt (Dec 15 2022 at 13:16):

You can know find boolp in the opam package coq-mathcomp-classical that has been factored out of coq-mathcomp-analysis.

Last updated: Sep 28 2023 at 11:01 UTC