max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/data/nat/basic): issue reported by @kha

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-17 13:17:30 -08:00
parent d41c403442
commit 422d43cf47
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/data/nat/basic.lean
View file

@ -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⟩