fix example

opencompl · Feb 24, 2024 · c927d6e · c927d6e
1 parent 949c696
commit c927d6e
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/Lean/Meta/Tactic/NormBv.lean b/src/Lean/Meta/Tactic/NormBv.lean
@@ -77,7 +77,8 @@ macro_rules
 example (x : BitVec 2) (y : BitVec 2) : x + y = y + x := by
   blast_bv with a a' b b';
   /-
-  b'ba'a: Bool
-⊢ concat (concat nil a') b' + concat (concat nil a) b = concat (concat nil a) b + concat (concat nil a') b'
+  b' b a' a: Bool
+  ⊢ concat (concat nil a') b' + concat (concat nil a) b
+    = concat (concat nil a) b + concat (concat nil a') b'
   -/
   sorry