Don't need to specify universe for mvcgen anymore

Changes

1 changed files (+1/-3)

• Sort.lean
  • @@ -2,9 +2,7 @@ import Std.Tactic.Do
    import Batteries.Data.Array.Pairwise import Mathlib.Data.Nat.Basic - -- Specify universe for α to avoid - -- https://github.com/leanprover/lean4/pull/10865 - variable {α : Type} [LinearOrder α] (A : Array α) + variable [LinearOrder α] (A : Array α) def BubbleSort := Id.run do let N := A.size