Skip to content

Commit

Permalink
chore: add full types
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser committed May 22, 2024
1 parent d062407 commit 01d9aa0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion SSA/Projects/InstCombine/LLVM/CLITests.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down

0 comments on commit 01d9aa0

Please sign in to comment.