From ea05ce7fe98e4b974944904062916b4c9a73ef56 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2015 15:03:18 -1000 Subject: [PATCH] fix(library/data/real/order): mark '2' as local notation --- library/data/real/order.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 627b32483..7dbddd440 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -15,7 +15,7 @@ open -[coercions] nat open eq eq.ops pnat local notation 0 := rat.of_num 0 local notation 1 := rat.of_num 1 -notation 2 := subtype.tag (of_num 2) dec_trivial +local notation 2 := subtype.tag (of_num 2) dec_trivial ----------------------------------------------------------------------------------------------------