diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean index 255760a..fb48e62 100644 --- a/Bookshelf/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -1,11 +1,11 @@ import Common.Real.Set -/-! # Apostol.Chapter_I_3 +/-! # Apostol.Chapter_I_03 A Set of Axioms for the Real-Number System -/ -namespace Apostol.Chapter_I_3 +namespace Apostol.Chapter_I_03 #check Archimedean #check Real.exists_isLUB @@ -640,4 +640,4 @@ the Archimedean property does not imply the least-upper-bound axiom. ###### TODO -/ -end Apostol.Chapter_I_3 \ No newline at end of file +end Apostol.Chapter_I_03 diff --git a/Bookshelf/Apostol/Chapter_I_03.tex b/Bookshelf/Apostol/Chapter_I_03.tex index 7488e0f..f62709c 100644 --- a/Bookshelf/Apostol/Chapter_I_03.tex +++ b/Bookshelf/Apostol/Chapter_I_03.tex @@ -3,9 +3,9 @@ \input{../../preamble} \newcommand{\link}[1]{\lean{../..} - {Bookshelf/Apostol/Chapter\_I\_3} - {Apostol.Chapter\_I\_3.#1} - {Chapter\_I\_3.#1} + {Bookshelf/Apostol/Chapter\_I\_03} % Location + {Apostol.Chapter\_I\_03.#1} % Namespace + {Chapter\_I\_03.#1} % Presentation } \begin{document} diff --git a/Bookshelf/Enderton.lean b/Bookshelf/Enderton.lean index 18d7966..30e3af7 100644 --- a/Bookshelf/Enderton.lean +++ b/Bookshelf/Enderton.lean @@ -1 +1 @@ -import Bookshelf.Enderton.Chapter0 \ No newline at end of file +import Bookshelf.Enderton.Chapter_0 diff --git a/Bookshelf/Enderton/Chapter0.lean b/Bookshelf/Enderton/Chapter_0.lean similarity index 99% rename from Bookshelf/Enderton/Chapter0.lean rename to Bookshelf/Enderton/Chapter_0.lean index d7f1c36..5ef44b3 100644 --- a/Bookshelf/Enderton/Chapter0.lean +++ b/Bookshelf/Enderton/Chapter_0.lean @@ -1,11 +1,11 @@ import Common.LTuple.Basic -/-! # Enderton.Chapter0 +/-! # Enderton.Chapter_0 Useful Facts About Sets -/ -namespace Enderton.Chapter0 +namespace Enderton.Chapter_0 /-- The following describes a so-called "generic" tuple. Like an `LTuple`, a generic @@ -275,4 +275,4 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k)) end -end Enderton.Chapter0 \ No newline at end of file +end Enderton.Chapter_0 diff --git a/Bookshelf/Enderton/Chapter0.tex b/Bookshelf/Enderton/Chapter_0.tex similarity index 79% rename from Bookshelf/Enderton/Chapter0.tex rename to Bookshelf/Enderton/Chapter_0.tex index d9a2caf..0405113 100644 --- a/Bookshelf/Enderton/Chapter0.tex +++ b/Bookshelf/Enderton/Chapter_0.tex @@ -3,9 +3,9 @@ \input{../../preamble} \newcommand{\link}[1]{\lean{../..} - {Bookshelf/Enderton/Chapter0} % Location - {Enderton.Chapter0.#1} % Namespace - {Chapter0.#1} % Presentation + {Bookshelf/Enderton/Chapter_0} % Location + {Enderton.Chapter_0.#1} % Namespace + {Chapter_0.#1} % Presentation } \begin{document} diff --git a/lake-manifest.json b/lake-manifest.json index 05cbe49..b5e122a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/jrpotter/bookshelf-docgen.git", "subDir?": null, - "rev": "291f71e6c520751d52832c95f47cbc059c77bfa7", + "rev": "80a4dc8d508161c859dbbb455f3855e051a28890", "name": "doc-gen4", - "inputRev?": "291f71e6c520751d52832c95f47cbc059c77bfa7"}}, + "inputRev?": "80a4dc8d508161c859dbbb455f3855e051a28890"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 1d2e9d9..fd5969f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ require std4 from git "6006307d2ceb8743fea7e00ba0036af8654d0347" require «doc-gen4» from git "https://github.com/jrpotter/bookshelf-docgen.git" @ - "291f71e6c520751d52832c95f47cbc059c77bfa7" + "80a4dc8d508161c859dbbb455f3855e051a28890" @[default_target] lean_lib «Bookshelf» {