From 1ebe2b590de77751bcd3aae816fa2baf5b371f7d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Nov 2016 10:42:13 -0800
Subject: [PATCH] feat(library/data/bitvec): define has_one for (bitvec 0) too.

---
 library/data/bitvec.lean | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 7c1b803f58..1aa598773f 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -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