We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent ed5109f commit 1973d9bCopy full SHA for 1973d9b
Fad/Chapter5-Ex.lean
@@ -217,7 +217,7 @@ def merge₁ (f : a → a → Ordering) : List a → List a → List a
217
y :: merge₁ f (x :: xs) ys
218
219
open Chapter1 (wrap unwrap single until') in
220
-open S52 in
+open Mergesort in
221
222
def sortBy (f : a → a → Ordering) : List a → List a
223
| [] => []
Fad/Chapter8.lean
@@ -11,7 +11,7 @@ namespace S1
11
12
/- 8.1 Minimum-height trees -/
13
14
-open Chapter5.S52 (halve length_halve_fst length_halve_snd pairWith)
+open Chapter5.Mergesort (halve length_halve_fst length_halve_snd pairWith)
15
open Chapter1 (wrap unwrap single until' concatMap)
16
open Chapter6 (foldl1)
17
open Chapter7 (minWith)
0 commit comments