Code

Add UIP to the SAW core prelude#1798

Code

Merged

mergify[bot] merged 2 commits intomasterGaloisInc/saw-script:masterfrom saw-core/uipGaloisInc/saw-script:saw-core/uipCopy head branch name to clipboardJan 11, 2023

+79-20

Commits

Commits on Jan 11, 2023

• added UIP as an axiom in SAW core; proved a number of properties using it, including properties for simplifying coercions

  

  Eddy Westbrook

  committed
  e77ff45

  Copy full SHA for e77ff45

• updated Coq translator to translate UIP and to correctly handle coerce__def and coerce__eq

  

  Eddy Westbrook

  committed
  2783a74

  Copy full SHA for 2783a74