danabra.mov
My solutions to Tao's Analysis I, formalized in Lean
add to analysisbook.lean file
+8
-2
+3
-2
CONTRIBUTING.md
+3
-2
CONTRIBUTING.md
···
7
7
8
8
1. Add the relevant file to `analysis/Analysis`
9
9
2. Copy a line of the `sections` definition in `book/lakefile.lean`, adapt it to the new section.
10
-
3. Adapt the line in the README
11
-
4. Add a line in `book/AnalysisBook/Home.lean`
10
+
3. Add a line to the `demoSite` definition in `book/AnalysisBook.lean` for the new section.
11
+
4. Adapt the line in the README
12
+
5. Add a line in `book/AnalysisBook/Home.lean`
+5
book/AnalysisBook.lean
+5
book/AnalysisBook.lean
···
62
62
"sec61" Book.Analysis.Section_6_1
63
63
"sec62" Book.Analysis.Section_6_2
64
64
"sec63" Book.Analysis.Section_6_3
65
+
"sec64" Book.Analysis.Section_6_4
66
+
"sec65" Book.Analysis.Section_6_5
67
+
"sec66" Book.Analysis.Section_6_6
68
+
"sec6e" Book.Analysis.Section_6_epilogue
69
+
"sec71" Book.Analysis.Section_7_1
65
70
66
71
def baseUrl := "https://teorth.github.io/analysis/docs/"
67
72