michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(init/nat): add spaces around inequalities

Browse source
This commit is contained in:
Floris van Doorn 2015-12-08 11:54:15 -05:00 committed by Leonardo de Moura
parent 377755e5ab
commit 14a2c8e444
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
hott/init/nat.hlean
View file

@ -17,15 +17,15 @@ namespace nat
| refl : le a a | refl : le a a
| step : Π {b}, le a b → le a (succ b) | step : Π {b}, le a b → le a (succ b)
infix `≤` := le infix ` ≤ ` := le
attribute le.refl [refl] attribute le.refl [refl]
definition lt [reducible] (n m : ℕ) := succ n ≤ m definition lt [reducible] (n m : ℕ) := succ n ≤ m
definition ge [reducible] (n m : ℕ) := m ≤ n definition ge [reducible] (n m : ℕ) := m ≤ n
definition gt [reducible] (n m : ℕ) := succ m ≤ n definition gt [reducible] (n m : ℕ) := succ m ≤ n
infix `<` := lt infix ` < ` := lt
infix `≥` := ge infix ` ≥ ` := ge
infix `>` := gt infix ` > ` := gt
definition pred [unfold 1] (a : nat) : nat := definition pred [unfold 1] (a : nat) : nat :=
nat.cases_on a zero (λ a₁, a₁) nat.cases_on a zero (λ a₁, a₁)