Add a fix for a test

leanprover-community · Dec 6, 2023 · c485120 · c485120
1 parent 13e1627
commit c485120
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/test/positivity.lean b/test/positivity.lean
@@ -323,7 +323,8 @@ example {r : ℝ≥0} (hr : 0 < r) : (0 : ℝ) < r := by positivity
 
 /- ## Other extensions -/
 
-example [Zero β] [PartialOrder β] [NonnegHomClass F α β] (f : F) (x : α) : 0 ≤ f x := by positivity
+example [Zero β] [PartialOrder β] [NDFunLike F α β] [NonnegHomClass F α β]
+    (f : F) (x : α) : 0 ≤ f x := by positivity
 
 example [OrderedSemiring S] [Semiring R] (abv : R → S) [IsAbsoluteValue abv] (x : R) :
     0 ≤ abv x := by