max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/nat_lemmas): add extra instances for short circuiting type class resolution

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-25 17:47:08 -08:00
parent 97dd2f34d5
commit efa760fc74
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/nat_lemmas.lean
View file

@ -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