Kazuhiko Sakaguchi comments

Results 306 comments of


                                            Kazuhiko Sakaguchi

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

Done modulo documentation

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

@Tragicus @CohenCyril FYI, this PR may break some of your backport PRs from Abel (or they are already broken because of math-comp/math-comp#1235). See also math-comp/Abel#93.

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

This PR and all the overlay PRs listed above are ready.

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

I will rebase this PR after merging #1245.

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

@CohenCyril This PR and its only overlay PR left (math-comp/Abel#93) are both ready. It's also blocking a potential improvement (simplification) of the archimedean mixin. Do you have time to take...

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

I removed the overlay.

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

> We should definitely open an issue on HB about deprecating HB structures/factories. @pi8027 since you needed it could you summarize the desired features in such an issue? Done: math-comp/hierarchy-builder#436

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

Since Cyril approved this PR, let me merge it and proceed to the next PR. Thanks @proux01 @affeldt-aist @CohenCyril for the help!

[Paper Artifact] Application of s-finite kernels to program semantics

``` File "./prob_lang.v", line 10, characters 0-33: Error: Cannot find a physical path bound to logical path lra with prefix mathcomp. ``` Isn't it just a matter of adding Algebra...

[Paper Artifact] Application of s-finite kernels to program semantics

Also, please consider fixing math-comp/algebra-tactics#62 before merging this.