We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6fb9c20 commit cc78164Copy full SHA for cc78164
src/Lean/Data/Fmt/Formatter.lean
@@ -825,7 +825,7 @@ partial def TaintedMeasure.resolve? : TaintedResolver σ τ := TaintedResolver.m
825
826
/--
827
Yields the measure in a non-tainted measure set with the lowest cost and amongst measures with the
828
-lowest cost, the one with the largest last line length.
+lowest cost, the one with the smallest last line length.
829
For a tainted measure, resolves the tainted measure to a regular measure.
830
-/
831
partial def MeasureSet.extractAtMostOne? (ms : MeasureSet τ) :
0 commit comments