From fb3150e69ddba0253d2bfc5602058b37333b68ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Apr 2019 07:21:17 -0700 Subject: [PATCH] chore(tests/playground): fix test --- tests/playground/rbmap.library.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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