Skip to content

separate digest from detailed documentation #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
yoshihiro503 merged 1 commit into from
Feb 15, 2025
Merged

separate digest from detailed documentation #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions Makefile.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,15 +138,14 @@ coq2html:
gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
gsed -i 's/\//\./g' depend.dot
../coq2html/tools/generate-hierarchy-graph.sh
../coq2html/coq2html \
find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/coq2html \
-hierarchy-graph hierarchy-graph.dot \
-dependency-graph depend.dot \
-title "Mathcomp Analysis" \
-d html/ -base mathcomp -Q theories analysis \
-coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \
-external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
-external https://math-comp.github.io/htmldoc/ mathcomp.algebra \
$(find . -not -path '*/.*' -name "*.v" -or -name "*.glob")
-external https://math-comp.github.io/htmldoc/ mathcomp.algebra

coq2html-clean:
rm -f */*.glob
2 changes: 1 addition & 1 deletion classical/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
(* set (i.e., of type set rT) *)
(* - indexed sets are rather named F *)
(* *)
(* Example of notations: *)
(* Examples of notations: *)
(* | Coq notations | | Meaning | *)
(* |-----------------------------:|---|:------------------------------------ *)
(* | set0 |==| $\emptyset$ *)
Expand Down
68 changes: 48 additions & 20 deletions reals/constructive_ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,41 +16,69 @@ From mathcomp Require Import mathcomp_extra signed.
(**md**************************************************************************)
(* # Extended real numbers $\overline{R}$ *)
(* *)
(* Given a type R for numbers, \bar R is the type R extended with symbols *)
(* -oo and +oo (notation scope: %E), suitable to represent extended real *)
(* numbers. When R is a numDomainType, \bar R is equipped with a canonical *)
(* porderType and operations for addition/opposite. When R is a *)
(* realDomainType, \bar R is equipped with a Canonical orderType. *)
(* Given a type R for numbers, `\bar R` is the type `R` extended with symbols *)
(* `-oo` and `+oo` (notation scope: `%E`), suitable to represent extended *)
(* real numbers. When `R` is a `numDomainType`, `\bar R` is equipped with a *)
(* canonical `porderType` and operations for addition/opposite. When `R` is a *)
(* `realDomainType`, `\bar R` is equipped with a canonical `orderType`. *)
(* *)
(* Naming convention: in definition/lemma identifiers, "e" stands for an *)
(* extended number and "y" and "Ny" for +oo ad -oo respectively. *)
(* extended number and "y" and "Ny" for `+oo` and `-oo` respectively. *)
(* *)
(* | Coq definitions | | | *)
(* Examples of notations: *)
(* | Coq definitions | | Meaning | *)
(* |-----------------------:|--|--------------------------------------------| *)
(* | `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$;|*)
(* | | | notation for extended `(R:Type)` | *)
(* | `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$| *)
(* | | | notation for `extended (R:Type)` | *)
(* | `r%:E` |==| injects real numbers into `\bar R` | *)
(* | `+%E, -%E, *%E` |==| addition/opposite/multiplication for extended|*)
(* | | | reals | *)
(* | `+%E, -%E, *%E` |==| addition/opposite/multiplication for | *)
(* | | | extended reals | *)
(* | `er_map (f : T -> T')` |==| the `\bar T -> \bar T'` lifting of `f` | *)
(* | `sqrte` |==| square root for extended reals | *)
(* | `` `\| x \|%E `` |==| the absolute value of `x` | *)
(* | `` `\| x \|%E `` |==| the absolute value of `x` | *)
(* | `x ^+ n` |==| iterated multiplication | *)
(* | `x *+ n` |==| iterated addition | *)
(* | `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition for | *)
(* | | | extended reals ($-\infty + +\infty = +\infty$ instead of $-\infty$)|*)
(* | `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition | *)
(* | | | ($-\infty + +\infty = +\infty$) | *)
(* | | | Import DualAddTheory for related lemmas | *)
(* | `x +? y` |==| the addition of the extended real numbers `x` and|*)
(* | | | and `y` is defined, i.e., it is neither $+\infty - \infty$|*)
(* | `x +? y` |==| the addition of `x` and `y` is defined | *)
(* | | | it is neither $+\infty - \infty$ | *)
(* | | | nor $-\infty + \infty$ | *)
(* | `x *? y` |==| the multiplication of the extended real numbers|*)
(* | | | `x` and `y` is not of the form $0 * +\infty$ or $0 * -\infty$|*)
(* | `x *? y` |==| the multiplication of `x` and `y` is not | *)
(* | | | of the form $0 * +\infty$ or $0 * -\infty$ | *)
(* | `(_ <= _)%E`, `(_ < _)%E`,|==| comparison relations for extended reals | *)
(* | `(_ >= _)%E`, `(_ > _)%E` | | | *)
(* | `(\sum_(i in A) f i)%E`|==| bigop-like notation in scope `%E` | *)
(* |`(\prod_(i in A) f i)%E`|==| bigop-like notation in scope `%E` | *)
(* | `maxe x y, mine x y` |==| notation for the maximum/minimum of two | *)
(* | | | extended real numbers | *)
(* | `maxe x y, mine x y` |==| notation for the maximum/minimum | *)
(* *)
(* Detailed documentation: *)
(* ``` *)
(* \bar R == coproduct of R and {+oo, -oo}; *)
(* notation for extended (R:Type) *)
(* r%:E == injects real numbers into \bar R *)
(* +%E, -%E, *%E == addition/opposite/multiplication for extended *)
(* reals *)
(* er_map (f : T -> T') == the \bar T -> \bar T' lifting of f *)
(* sqrte == square root for extended reals *)
(* `| x |%E == the absolute value of x *)
(* x ^+ n == iterated multiplication *)
(* x *+ n == iterated addition *)
(* +%dE, (x *+ n)%dE == dual addition/dual iterated addition for *)
(* extended reals (-oo + +oo = +oo instead of -oo) *)
(* Import DualAddTheory for related lemmas *)
(* x +? y == the addition of the extended real numbers x and *)
(* and y is defined, i.e., it is neither +oo - oo *)
(* nor -oo + oo *)
(* x *? y == the multiplication of the extended real numbers *)
(* x and y is not of the form 0 * +oo or 0 * -oo *)
(* (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals *)
(* (_ >= _)%E, (_ > _)%E *)
(* (\sum_(i in A) f i)%E == bigop-like notation in scope %E *)
(* (\prod_(i in A) f i)%E == bigop-like notation in scope %E *)
(* maxe x y, mine x y == notation for the maximum/minimum of two *)
(* extended real numbers *)
(* ``` *)
(* *)
(* ## Signed extended real numbers *)
(* ``` *)
Expand Down
Loading