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

feat(library/data/bitvec): define has_one for (bitvec 0) too.

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-22 10:42:13 -08:00
parent b35aef2895
commit 1ebe2b590d
1 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
library/data/bitvec.lean
View file

@ -103,18 +103,25 @@ section arith
def sub : bitvec n → bitvec n → bitvec n
| x y := prod.snd (sbb x y ff)
instance : has_zero (bitvec n) := has_zero.mk zero
instance : has_one (bitvec (succ n)) := has_one.mk one
instance : has_add (bitvec n) := has_add.mk add
instance : has_sub (bitvec n) := has_sub.mk sub
instance : has_neg (bitvec n) := has_neg.mk neg
instance : has_zero (bitvec n) := ⟨zero⟩
/- Remark: we used to have the instance has_one only for (bitvec (succ n)).
Now, we define it for all n to make sure we don't have to solve unification problems such as:
succ ?n =?= (bit0 (bit1 one)) -/
instance : has_one (bitvec n) :=
match n with
| 0 := ⟨zero⟩
| (nat.succ n) := ⟨one⟩
end
instance : has_add (bitvec n) := ⟨add⟩
instance : has_sub (bitvec n) := ⟨sub⟩
instance : has_neg (bitvec n) := ⟨neg⟩
def mul : bitvec n → bitvec n → bitvec n
| x y :=
let f := λr b, cond b (r + r + y) (r + r) in
list.foldl f 0 (to_list x)
instance : has_mul (bitvec n) := has_mul.mk mul
instance : has_mul (bitvec n) := ⟨mul⟩
end arith
section comparison