analysis

analysis copied to clipboard

https://github.com/math-comp/analysis/blob/master/README.md#mathematical-structures does not display the mathematical structures of measure theory for example

affeldt-aist

fsbigop.v review

3

I've done a review of the fsbigop.v file. Looks pretty reasonable. There are a couple mechanical things, and then a couple more general questions: @affeldt-aist, not sure who else should...

zstone1

Backport Enrico's inline "!!" refining for the have tactic to mathcomp?

1

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/posnum.v#L20

CohenCyril

I get a weird error message after completing a `near` proof, but before Unshelving: > TypeError: Cannot read property 'before' of null Not sure what it's talking about, and everything...

zstone1

there is a canonical declaration and a coercion for `measure_additive_measure` https://github.com/math-comp/analysis/blob/68eea40c6cbcb1882762954361476b9b2a0dadac/theories/measure.v#L556 https://github.com/math-comp/analysis/blob/68eea40c6cbcb1882762954361476b9b2a0dadac/theories/measure.v#L561 still it often needs to be explicitly mentioned when used, e.g.: https://github.com/math-comp/analysis/blob/68eea40c6cbcb1882762954361476b9b2a0dadac/theories/measure.v#L828 https://github.com/math-comp/analysis/blob/68eea40c6cbcb1882762954361476b9b2a0dadac/theories/measure.v#L851 there is also a warning...

affeldt-aist

Inclusion in the Coq Platform

5

Dear math-comp Team, @palmskog requested here: (https://github.com/coq/platform/issues/21) to include your development into the Coq Platform, which is the standard user facing distribution of Coq. Coq Platform has a "full" and...

MSoegtropIMC

Endow R^o, C^o (which are copies of R, C) with structures

2

For now it is not clear how to proceed: is it broken or is documentation missing? Many lines in [this](https://github.com/math-comp/analysis/blob/3edd010fa7b101f449c6f364e0dfacb51b546496/theories/cauchyetoile.v#L194) file declare instances for C^o, using its convertibility with C...

amahboubi

TODO (alternatives): - [ ] Lock the definition of `diff`using a module type : https://github.com/math-comp/analysis/blob/99d2078cc61335967a5c39594b9f2853fe3a8c25/derive.v#L46-L48 - [ ] Use canonical structures instead of typeclasses for automatic derive

CohenCyril

Rework landau's documentation and naming convention

2

This is related to #101. [NB(rei): PR which has been merged] [NB(rei): partially addressed by PR #216 ] Since we force user to use the equational notations by removing the...

drouhling

The notations near and locally are too unstable.

3

Redo filters in mem_pred style. PR soon!

CohenCyril