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

feat(library/init/nat): add missing decidable_ge and decidable_lt

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-13 08:08:54 -07:00
parent 82eada7d56
commit a24d4e47cd
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/nat.lean
View file

@ -250,10 +250,14 @@ namespace nat
eq.rec_on aux (le_of_lt h))) eq.rec_on aux (le_of_lt h)))
definition gt [reducible] a b := lt b a definition gt [reducible] a b := lt b a
definition decidable_gt [instance] : decidable_rel gt :=
_
notation a > b := gt a b notation a > b := gt a b
definition ge [reducible] a b := le b a definition ge [reducible] a b := le b a
definition decidable_ge [instance] : decidable_rel ge :=
_
notation a ≥ b := ge a b notation a ≥ b := ge a b