From 422d43cf472fc3fb7ccac2171937d082f802add2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Dec 2016 13:17:30 -0800 Subject: [PATCH] fix(library/init/data/nat/basic): issue reported by @kha --- library/init/data/nat/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 129bf8afe8..a2d2d7b0a3 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -17,8 +17,8 @@ inductive less_than (a : ℕ) : ℕ → Prop instance : has_le ℕ := ⟨nat.less_than⟩ -@[reducible] protected def le (n m : ℕ) := n ≤ m -@[reducible] protected def lt (n m : ℕ) := succ n ≤ m +@[reducible] protected def le (n m : ℕ) := nat.less_than n m +@[reducible] protected def lt (n m : ℕ) := nat.less_than (succ n) m instance : has_lt ℕ := ⟨nat.lt⟩