Skip to content

Commit

Permalink
rm diagramms from README (#1406)
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist authored Nov 22, 2024
1 parent e1d6540 commit ff1b91c
Show file tree
Hide file tree
Showing 6 changed files with 1 addition and 18 deletions.
19 changes: 1 addition & 18 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ We try to preserve backward compatibility as best as we can.
Each file is documented in its header in ASCII.

[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_7_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones.

Overview presentations:
- [Classical Analysis with Coq](https://perso.crans.org/cohen/CoqWS2018.pdf) (2018)
Expand All @@ -110,24 +111,6 @@ Other work using MathComp-Analysis:
- [Experimenting with an intrinsically-typed probabilistic programming language in Coq](https://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf) (2023)
- [Taming Differentiable Logics with Coq Formalisation](https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.4/LIPIcs.ITP.2024.4.pdf) (2024)

## Mathematical structures

MathComp-Analysis adds mathematical structures on top of MathComp's ones.
The following inheritance diagram displays the resulting hierarchy as of version 1.1.0
(excluding most MathComp structures).
The structures introduced by MathComp-Analysis are highlighted.
(See `topology.v`, `normedtype.v`, `reals.v`, `measure.v`.)

<img width="600" alt="Main_inheritance_graph" src="etc/hierarchy_main.1.1.0.png">


### Hierarchies of functions

| Functions | Functions with a finite image | Measures | Kernels |
|:----------:|:-----------------------------:|:--------:|:-------:|
| <img width="300" alt="Functions" src="etc/hierarchy_functions.1.1.0.png"> | <img width="200" alt="Functions_with_a_finite_image" src="etc/hierarchy_fimfun.1.1.0.png"> | <img width="300" alt="Measures" src="etc/hierarchy_measure.1.1.0.png"> | <img width="200" alt="Kernels" src="etc/hierarchy_kernel.1.1.0.png"> |
| (see `functions.v`) | (see `cardinality.v`, `lebesgue_integral.v`) | (see `measure.v`, `charge.v`) | (see `kernel.v`) |

## Development information

[Detailed requirements and installation procedure](INSTALL.md)
Expand Down
Binary file removed etc/hierarchy_fimfun.1.1.0.png
Binary file not shown.
Binary file removed etc/hierarchy_functions.1.1.0.png
Binary file not shown.
Binary file removed etc/hierarchy_kernel.1.1.0.png
Binary file not shown.
Binary file removed etc/hierarchy_main.1.1.0.png
Binary file not shown.
Binary file removed etc/hierarchy_measure.1.1.0.png
Binary file not shown.

0 comments on commit ff1b91c

Please sign in to comment.