-
Notifications
You must be signed in to change notification settings - Fork 47
Home
affeldt-aist edited this page Jun 26, 2024
·
413 revisions
-
Documentation (link inside the README)
Date: between 2024-06-26 (Paris Time)
-
Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2024-04-16-Meeting)
-
News:
- MathComp-Analysis 1.2.0 released 3 weeks ago (https://github.com/math-comp/analysis/releases/tag/1.2.0)
- Alessandro's presentation at TYPES: https://alessandrobruni.name/papers/24-mca_proba.pdf
- corollary to FTC1 PR #1246
- "poor man's FTC2"
- under review
-
take a decision about https://github.com/math-comp/analysis/pull/1191 (topology without pointed types)
-
questions raised recently:
- is it ok for us (users of the standard Coq library) to extend the
core
Hint database? - generalization of
{mfun _ >-> _}
? (as in PR 672)
- is it ok for us (users of the standard Coq library) to extend the
-
work in progress about
measure.v
: -
PR triaging:
- merge the Banach-Steinhaus PR?
-
to_set
vs.xsection
PR 1248 - easy corollary to FTC1 PR 1250
- new Zorn's PR 1198 (stalled by lack of time)
- Documentation:
- Simplification of the filter layer
- Issue related to Landau:
- typechecking in Landau notations using
derive.v
- typechecking in Landau notations using
- 2024
- 2023
- 2022
- 2021
- 2020
- 2019
- 2019-12-16
- 2019-09-26
- 2019-07-18
- 2019-06-28
- 2019-06-27
- 2019-06-07
- 2019-05-27
- 2019-05-14
- 2019-05-09
- 2019-03-26
- 2019-02-27 (minutes lost?)
- 2018