From ec53256c07f536448422e25758e7654b0c40f0b8 Mon Sep 17 00:00:00 2001 From: Benjamin Jones Date: Thu, 9 Jan 2025 18:53:11 -0800 Subject: [PATCH] Fix minor typographic error in S01_Basics.lean The placement of the final text block's `-/` causes it to be rendered in the textbook. --- MIL/C07_Hierarchies/S01_Basics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean index a60c337..3adaddf 100644 --- 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: