Merge remote-tracking branch 'origin/master' into getLsbD_getElem_simp

opencompl · Sep 18, 2024 · 708b8a7 · 708b8a7
2 parents 3be0037 + daf24ff
commit 708b8a7
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -243,6 +243,15 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
 
+@[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
+  cases b <;> cases b' <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl

diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -46,6 +46,30 @@
      "position": {"line": 9, "character": 11}},
     "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "4",
+   "label": "BitVec.ofBool_and_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
+  {"sortText": "5",
+   "label": "BitVec.ofBool_or_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
+  {"sortText": "6",
+   "label": "BitVec.ofBool_xor_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_xor_ofBool"}}}},
+  {"sortText": "7",
    "label": "BitVec.ofBoolListBE",
    "kind": 3,
    "documentation":