Code

getLsb_sshiftRight#3

Code

Closed

bollu wants to merge 15 commits intomasteropencompl/lean4:masterfrom bitvec-theoremsopencompl/lean4:bitvec-theoremsCopy head branch name to clipboard

+456-1

Commits

Commits on May 13, 2024

• wip: shifting lemmas

  bollu

  committed
  cab7583

  Copy full SHA for cab7583

• feat: move Int bitwise lemmas into basic

  bollu

  committed
  2f17f0d

  Copy full SHA for 2f17f0d

• Revert "feat: move Int bitwise lemmas into basic"

  Show description for 2e95bbe
  bollu

  committed
  2e95bbe

  Copy full SHA for 2e95bbe

• feat: grab the biwise lemmas

  bollu

  committed
  2fa2081

  Copy full SHA for 2fa2081

• feat: port bitwise lemmas from mathlib4 into Lean

  bollu

  committed
  7d4afe9

  Copy full SHA for 7d4afe9

Commits on May 14, 2024

• feat: write theory in terms of toInt

  bollu

  committed
  6be4817

  Copy full SHA for 6be4817

• feat: write proof sketch necessary

  bollu

  committed
  d0e08c4

  Copy full SHA for d0e08c4

• checkpoint

  bollu

  committed
  b013df0

  Copy full SHA for b013df0

Commits on May 15, 2024

• feat: build up testBit for int theory and modulo 2 theory

  bollu

  committed
  6ba1cc1

  Copy full SHA for 6ba1cc1

• feat: checkpoint

  bollu

  committed
  239e3c5

  Copy full SHA for 239e3c5

• feat: show easy cases unconditionally

  bollu

  committed
  1029f69

  Copy full SHA for 1029f69

• feat: more progress

  bollu

  committed
  968b271

  Copy full SHA for 968b271

• checkpoint

  bollu

  committed
  187d150

  Copy full SHA for 187d150

• feat: finish proof

  bollu

  committed
  2940f48

  Copy full SHA for 2940f48

• feat: cleaned up proof

  Show description for 7117789
  bollu

  committed
  7117789

  Copy full SHA for 7117789