Fix comment typo

Changes

1 changed files (+1/-1)

• Sort.lean
  • @@ -33,7 +33,7 @@ theorem kadane_correct A : is_max_subarray A.toList (kadane A) := by
    apply Id.of_wp_run_eq h mvcgen case inv1 => - -- cur might be negative so the loop invariant can only guarentee ∀ i < xs.prefix.length + -- cur might be negative so the loop invariant can only guarantee ∀ i < xs.prefix.length exact ⇓⟨xs, ans, cur⟩ => ⌜0 ≤ ans ∧ (∃ i ≤ xs.prefix.length, (xs.prefix.drop i).sum = cur) ∧ (∀ i < xs.prefix.length, (xs.prefix.drop i).sum ≤ cur) ∧ is_max_subarray xs.prefix ans⌝ all_goals mleave case vc1.step ih =>