chore: add missing def to simp set and use full types (prepare for le…

…an 4.9) (#326)

These changes issues in the 4.9 update. As they are independent and
should pass CI already, we factored these out.

SSA/Projects/InstCombine/LLVM/CLITests.lean

@@ -200,7 +200,7 @@ match ctxt, values with
     let valuation' := mkValuation tys valsVec
     match ty with
       | .bitvec (.concrete w) =>
-         let newTy : toType (.bitvec (.concrete w)) := Option.map (BitVec.ofInt w) val
+         let newTy : toType (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)) := Option.map (BitVec.ofInt w) val
          Ctxt.Valuation.snoc valuation' newTy
 
 def ConcreteCliTest.eval (test : ConcreteCliTest) (values : Vector (Option Int) test.context.length) :

SSA/Projects/Scf/ScfFunctor.lean

@@ -477,7 +477,7 @@ abbrev instHadd : HAdd ⟦ScfFunctor.Arith.Ty.int⟧ ⟦ScfFunctor.Arith.Ty.int
 open Scf in
 open Arith in
 theorem correct : Com.denote (lhs v0) Γv = Com.denote (rhs v0) Γv := by
-  simp only [lhs, rhs, for_, axpy, cst]
+  simp only [lhs, rhs, for_, axpy, cst, add]
   simp_peephole at Γv
   intros A B
   simp only [Ctxt.Valuation.snoc, Var.casesOn, Ctxt.get?, Var.zero_eq_last, cast_eq]