aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Published 20 hours ago • verified publisher icon AeneasVerif

Add theorems about `List`, `Array`, `Vector`, `BitVec` and improve `zmodify`

Open sonmarcho opened this issue 7 months ago • 0 comments
trafficstars

This PR does the following:

  • introduce many lemmas about List, Array, Vector and BitVec
  • introduce a new tactic simp_scalar to simplify arithmetic expressions
  • improve zmodify to use scalar_tac as a discharger for the conditional rewritings

sonmarcho avatar Apr 21 '25 12:04 sonmarcho