Fix minor typographic error in S01_Basics.lean

The placement of the final text block's `-/` causes it to be rendered in the textbook.
avigad · Jan 20, 2025 · 331c717 · 331c717
1 parent 6a626c5
commit 331c717
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean
@@ -759,7 +759,7 @@ As an exercise, you can come back to the order relation hierarchy you built abov
 to incorporate a type class ``LT₁`` carrying the Less-Than notation ``<₁`` and make sure
 that every preorder comes with a ``<₁`` which has a default value built from ``≤₁`` and a
 ``Prop``-valued field asserting the natural relation between those two comparison operators.
--/
+TEXT. -/
 
 -- SOLUTIONS: