From 616f2d9b823f0f01910ea6a4cb735c8a40b4c53a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Nov 2014 17:33:42 -0800 Subject: [PATCH] fix(library/data/nat/div): notation should be local --- library/data/nat/div.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 612fc718b..baa80edc7 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -399,7 +399,7 @@ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure p private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure.wf pr₂) 20 -- Remark: we use intro_k to be able to execute gcd efficiently in the kernel instance pair_nat.lt.wf -- Remark: instance will not be saved in .olean -infixl `≺`:50 := pair_nat.lt +infixl [local] `≺`:50 := pair_nat.lt private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) := mod_lt (succ_pos y₁)