From efa760fc740553acafd0412cd986bc21653eb224 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Nov 2016 17:47:08 -0800 Subject: [PATCH] feat(library/init/nat_lemmas): add extra instances for short circuiting type class resolution --- library/init/nat_lemmas.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/library/init/nat_lemmas.lean b/library/init/nat_lemmas.lean index ede2ee548f..bb676267c1 100644 --- a/library/init/nat_lemmas.lean +++ b/library/init/nat_lemmas.lean @@ -545,4 +545,14 @@ protected lemma one_le_bit0 : ∀ (n : ℕ), n ≠ 0 → 1 ≤ bit0 n eq.symm (nat.bit0_succ_eq n) ▸ this, succ_le_succ (zero_le (succ (bit0 n))) +/- Extra instances to short-circuit type class resolution -/ +instance : add_comm_monoid nat := by apply_instance +instance : add_monoid nat := by apply_instance +instance : monoid nat := by apply_instance +instance : comm_monoid nat := by apply_instance +instance : comm_semigroup nat := by apply_instance +instance : semigroup nat := by apply_instance +instance : add_comm_semigroup nat := by apply_instance +instance : add_semigroup nat := by apply_instance + end nat