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

feat(library/data/num): show that num has decidable equality

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-31 17:47:07 -10:00
parent 63b93cf762
commit 3b19de1974
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/data/num.lean
View file

@ -510,3 +510,14 @@ namespace pos_num
end end
end pos_num end pos_num
namespace num
open pos_num
theorem decidable_eq [instance] : ∀ (a b : num), decidable (a = b)
| zero zero := inl rfl
| zero (pos b) := inr (by contradiction)
| (pos a) zero := inr (by contradiction)
| (pos a) (pos b) :=
if H : a = b then inl (by rewrite H) else inr (suppose pos a = pos b, begin injection this, contradiction end)
end num