Code

feat: BitVec.toInt_sshiftRight#39

Code

Draft

mhk119 wants to merge 19 commits intomasteropencompl/lean4:masterfrom sshiftrightopencompl/lean4:sshiftrightCopy head branch name to clipboard

+125

Commits

Commits on Feb 16, 2025

• feat: BitVec.toFin/toInt (BitVec.ushiftRight x)

  Show description for 38ef4e4
  

  mhk119

  authored and

  tobiasgrosser

  committed
  38ef4e4

  Copy full SHA for 38ef4e4

• Update src/Init/Data/BitVec/Lemmas.lean

  Show description for 49f4cfa
  

  bollu

  and

  tobiasgrosser

  committed
  49f4cfa

  Copy full SHA for 49f4cfa

• Update src/Init/Data/BitVec/Lemmas.lean

  Show description for 5ee463e
  

  bollu

  and

  tobiasgrosser

  committed
  5ee463e

  Copy full SHA for 5ee463e

• progress

  

  mhk119

  authored and

  tobiasgrosser

  committed
  12757f1

  Copy full SHA for 12757f1

• progres

  

  mhk119

  authored and

  tobiasgrosser

  committed
  6106907

  Copy full SHA for 6106907

• more attempst

  

  mhk119

  authored and

  tobiasgrosser

  committed
  8ba58ca

  Copy full SHA for 8ba58ca

• progress

  

  mhk119

  authored and

  tobiasgrosser

  committed
  facda43

  Copy full SHA for facda43

• thm proved finally

  

  mhk119

  authored and

  tobiasgrosser

  committed
  4a775d7

  Copy full SHA for 4a775d7

• small change

  

  mhk119

  authored and

  tobiasgrosser

  committed
  5c3d2de

  Copy full SHA for 5c3d2de

• small change

  

  mhk119

  authored and

  tobiasgrosser

  committed
  9b5ad73

  Copy full SHA for 9b5ad73

• extra stuff

  

  mhk119

  authored and

  tobiasgrosser

  committed
  2db7a25

  Copy full SHA for 2db7a25

• make it work

  tobiasgrosser

  committed
  dd214af

  Copy full SHA for dd214af

• make it work

  tobiasgrosser

  committed
  222bfc4

  Copy full SHA for 222bfc4

• restructure proof

  tobiasgrosser

  committed
  dfac93d

  Copy full SHA for dfac93d

Commits on Feb 17, 2025

• restructure proof

  tobiasgrosser

  committed
  8c57464

  Copy full SHA for 8c57464

• WIP

  tobiasgrosser

  committed
  dbd31e0

  Copy full SHA for dbd31e0

• WIP

  tobiasgrosser

  committed
  6c1b916

  Copy full SHA for 6c1b916

• Update src/Init/Data/Int/Lemmas.lean

  tobiasgrosser

  authored
  9798c82

  Copy full SHA for 9798c82

• WIP

  tobiasgrosser

  committed
  e4353a7

  Copy full SHA for e4353a7