From 540eb32b34d13cbe6d9dd410bdb6585638030e52 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 15 Jul 2026 11:28:10 +0300 Subject: [PATCH] fix: close module doc blocks in Section_3_2 and Section_3_5 /-! headers were closed with --/ instead of -/. Co-authored-by: Cursor --- Analysis/Section_3_2.lean | 2 +- Analysis/Section_3_5.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Analysis/Section_3_2.lean b/Analysis/Section_3_2.lean index ca2690f6e..cc1cc28ea 100644 --- a/Analysis/Section_3_2.lean +++ b/Analysis/Section_3_2.lean @@ -24,7 +24,7 @@ Users of the companion who have completed the exercises in this section are welc - (Add tip here) ---/ +-/ namespace Chapter3 diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean index 792e88a40..7fb747590 100644 --- a/Analysis/Section_3_5.lean +++ b/Analysis/Section_3_5.lean @@ -25,7 +25,7 @@ Users of the companion who have completed the exercises in this section are welc - (Add tip here) ---/ +-/ namespace Chapter3