Skip to content
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

minimal changes to documentation to test coq2html #1108

Merged
merged 6 commits into from
Jan 8, 2024
Merged

minimal changes to documentation to test coq2html #1108

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
81c7e6a
test a few files
affeldt-aist Nov 24, 2023
c845439
fix
affeldt-aist Dec 8, 2023
a434900
fix
affeldt-aist Dec 9, 2023
ed17518
fix
affeldt-aist Dec 9, 2023
2f6c482
fix
affeldt-aist Jan 8, 2024
6ff15ac
fix
affeldt-aist Jan 8, 2024
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
26 changes: 16 additions & 10 deletions classical/boolp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,18 @@

From mathcomp Require Import all_ssreflect.

(******************************************************************************)
(* Classical Logic *)
(***md*************************************************************************)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, are th three stars before md mandatory? why not just two? (coqdoc syntax is (** IIRC so not sure a third star is needed)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's arbitrary. No strong reason I think.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we don't really care because there are stars all along the line. But in case we wouldn't use block comments, with stars all around, but just start (* and closing *) syntax, the less stars the better I'd say.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We'll clarify this on Friday.

(* # 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
View file
Open in desktop
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
Loading