diff --git a/tests/playground/rbmap.library.lean b/tests/playground/rbmap.library.lean index f91e97a051..2c845d006f 100644 --- a/tests/playground/rbmap.library.lean +++ b/tests/playground/rbmap.library.lean @@ -1,4 +1,4 @@ -@[reducible] def Map : Type := RBMap Nat Bool (<) +@[reducible] def Map : Type := RBMap Nat Bool (λ a b, a < b) def mkMapAux : Nat → Map → Map | 0 m := m