Code

feat: getLsb_signExtend#4187

Code

Merged

kim-em merged 11 commits intoleanprover:masterleanprover/lean4:masterfrom opencompl:getLsb_signExtendopencompl/lean4:getLsb_signExtendCopy head branch name to clipboardJun 5, 2024

Commits

Commits on Jun 2, 2024

• feat: getLsb_signExtend

  bollu

  committed
  d2340d6

  Copy full SHA for d2340d6

Commits on Jun 3, 2024

• Apply suggestions from code review

  Show description for 0d2aa1b
  

  bollu

  and

  tobiasgrosser

  authored
  0d2aa1b

  Copy full SHA for 0d2aa1b

• chore: delete lemmas about sext, will upstream as a separate patch

  bollu

  committed
  2d2e1b7

  Copy full SHA for 2d2e1b7

• formatting

  alexkeizer

  committed
  2486db1

  Copy full SHA for 2486db1

• slight cleanup

  alexkeizer

  committed
  981fbca

  Copy full SHA for 981fbca

Commits on Jun 4, 2024

• Apply suggestions from code review

  Show description for 1118b25
  

  bollu

  and

  kim-em

  authored
  1118b25

  Copy full SHA for 1118b25

• chore: truncate -> zext, neg -> not, change comments to sentences

  bollu

  committed
  851156e

  Copy full SHA for 851156e

• chore: decrease swapping between rw and simp only

  bollu

  committed
  43d35ad

  Copy full SHA for 43d35ad

• chore: leftover truncate -> zext

  bollu

  committed
  5e1648a

  Copy full SHA for 5e1648a

• chore: remove reundant parens

  bollu

  committed
  2976b1a

  Copy full SHA for 2976b1a

• chore: address tobias' comments

  bollu

  committed
  5ea067e

  Copy full SHA for 5ea067e