feat: add Bitvec notation for and/or/xor/not (#5340)

leanprover-community · Jun 21, 2023 · 236422b · 236422b
1 parent 862226b
commit 236422b
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/Mathlib/Data/Bitvec/Defs.lean b/Mathlib/Data/Bitvec/Defs.lean
@@ -131,6 +131,18 @@ protected def xor : Bitvec n → Bitvec n → Bitvec n :=
   map₂ xor
 #align bitvec.xor Bitvec.xor
 
+instance : Complement (Bitvec n) :=
+⟨Bitvec.not⟩
+
+instance : AndOp (Bitvec n) :=
+⟨Bitvec.and⟩
+
+instance : OrOp (Bitvec n) :=
+⟨Bitvec.or⟩
+
+instance : Xor (Bitvec n) :=
+⟨Bitvec.xor⟩
+
 end Bitwise
 
 /-! ### Arithmetic operators -/