Skip to content

Commit

Permalink
minimal changes to documentation to test coq2html (math-comp#1108)
Browse files Browse the repository at this point in the history
* test a few files
  • Loading branch information
affeldt-aist committed Jan 9, 2024
1 parent 6758203 commit 412dacd
Show file tree
Hide file tree
Showing 38 changed files with 746 additions and 542 deletions.
26 changes: 16 additions & 10 deletions classical/boolp.v
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,18 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

(******************************************************************************)
(* Classical Logic *)
(***md*************************************************************************)
(* # Classical Logic *)
(* *)
(* This file provides the axioms of classical logic and tools to perform *)
(* classical reasoning in the Mathematical Compnent framework. The three *)
(* axioms are taken from the standard library of Coq, more details can be *)
(* found in Section 5 of *)
(* Reynald Affeldt, Cyril Cohen, Damien Rouhling: *)
(* Formalization Techniques for Asymptotic Reasoning in Classical Analysis. *)
(* Journal of Formalized Reasoning, 2018 *)
(* - R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for *)
(* Asymptotic Reasoning in Classical Analysis. JFR 2018 *)
(* *)
(* * Axioms *)
(* ## Axioms *)
(* ``` *)
(* functional_extensionality_dep == functional extensionality (on dependently *)
(* typed functions), i.e., functions that are pointwise *)
(* equal are equal *)
Expand All @@ -27,14 +27,19 @@ From mathcomp Require Import all_ssreflect.
(* constructive_indefinite_description == existential in Prop (ex) implies *)
(* existential in Type (sig) *)
(* cid := constructive_indefinite_description (shortcut) *)
(* --> A number of properties are derived below from these axioms and are *)
(* ``` *)
(* *)
(* A number of properties are derived below from these axioms and are *)
(* often more pratical to use than directly using the axioms. For instance *)
(* propext, funext, the excluded middle (EM),... *)
(* *)
(* * Boolean View of Prop *)
(* ## Boolean View of Prop *)
(* ``` *)
(* `[< P >] == boolean view of P : Prop, see all lemmas about asbool *)
(* ``` *)
(* *)
(* * Mathematical Components Structures *)
(* ## Mathematical Components Structures *)
(* ``` *)
(* {classic T} == Endow T : Type with a canonical eqType/choiceType. *)
(* This is intended for local use. *)
(* E.g., T : Type |- A : {fset {classic T}} *)
Expand All @@ -43,8 +48,9 @@ From mathcomp Require Import all_ssreflect.
(* {eclassic T} == Endow T : eqType with a canonical choiceType. *)
(* On the model of {classic _}. *)
(* See also the lemmas Peq and eqPchoice. *)
(* ``` *)
(* *)
(* --> Functions into a porderType (resp. latticeType) are equipped with *)
(* Functions into a porderType (resp. latticeType) are equipped with *)
(* a porderType (resp. latticeType), (f <= g)%O when f x <= g x for all x, *)
(* see lemma lefP. *)
(******************************************************************************)
Expand Down
6 changes: 4 additions & 2 deletions classical/cardinality.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ From HB Require Import structures.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.

(******************************************************************************)
(* Cardinality *)
(***md*************************************************************************)
(* # Cardinality *)
(* *)
(* This file provides an account of cardinality properties of classical sets. *)
(* This includes standard results of set theory such as the Pigeon Hole *)
Expand All @@ -16,6 +16,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
(* only relations A #<= B and A #= B to compare the cardinals of two sets *)
(* (on two possibly different types). *)
(* *)
(* ``` *)
(* A #<= B == the cardinal of A is smaller or equal to the one of B *)
(* A #>= B := B #<= A *)
(* A #= B == the cardinal of A is equal to the cardinal of B *)
Expand All @@ -32,6 +33,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
(* A.`1 := [fset x.1 | x in A] *)
(* A.`2 := [fset x.2 | x in A] *)
(* {fimfun aT >-> T} == type of functions with a finite image *)
(* ``` *)
(* *)
(******************************************************************************)

Expand Down
Loading

0 comments on commit 412dacd

Please sign in to comment.