Stream: math-comp analysis

Topic: boolp


view this post on Zulip Pierre-Yves Strub (Feb 17 2022 at 13:57):

Hi. What is the status of boolp?

view this post on Zulip Pierre-Yves Strub (Feb 17 2022 at 13:57):

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

view this post on Zulip Pierre-Yves Strub (Feb 17 2022 at 13:57):

(I might need it in some dev.)

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:00):

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

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:00):

a new classical-mathcomp repo or something?

view this post on Zulip 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 ;)

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:00):

We should do some cleaning in it though...

view this post on Zulip 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)

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:01):

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

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:02):

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

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:02):

(but no topological spaces etc)

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:02):

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

view this post on Zulip Pierre-Yves Strub (Feb 17 2022 at 14:03):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Pierre-Yves Strub (Feb 25 2022 at 07:45):

Yep.

view this post on Zulip 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: Mar 28 2024 at 16:02 UTC