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

fix(library/algebra/numeral): remove redundant definitions

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-13 16:33:52 -07:00
parent a25b43f1e8
commit 06e35b4863
1 changed files with 0 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
library/algebra/numeral.lean
View file

@ -3,21 +3,6 @@ open algebra
variable {A : Type}
definition zero [s : has_zero A] : A :=
has_zero.zero A
definition one [s : has_one A] : A :=
has_one.one A
definition add [s : has_add A] : A → A → A :=
has_add.add
definition bit0 [s : has_add A] (a : A) : A :=
add a a
definition bit1 [s₁ : has_add A] [s₂ : has_one A] (a : A) : A :=
add (add a a) one
-- variables [s : ring A]
-- set_option pp.all true
-- check bit1 (bit0 (one : A))