last changes

Author: hargoniX

Diff for: src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -162,7 +162,6 @@ where
       | UInt16.toBitVec x => fvarId? x
       | UInt32.toBitVec x => fvarId? x
       | UInt64.toBitVec x => fvarId? x
-      | USize.toBitVec x => fvarId? x
       | _ => none
   fvarId? (expr : Expr) : Option FVarId :=
     match expr with

Diff for: src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean

@@ -141,7 +141,7 @@ where
       return goal
 
   /--
-  Builds an expression of type: `System.Platform.numBits = const` from the hypotheses in the context
+  Builds an expression of type: `const = System.Platform.numBits` from the hypotheses in the context
   if possible.
   -/
   findNumBitsEq (goal : MVarId) : MetaM (Option (Nat × Expr)) := do