From 3b19de1974b584f340777a5d6fc9c3de48c9245a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2015 17:47:07 -1000 Subject: [PATCH] feat(library/data/num): show that num has decidable equality --- library/data/num.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/library/data/num.lean b/library/data/num.lean index 1723b5c62..7746fedf3 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -510,3 +510,14 @@ namespace pos_num end 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