Commits

Branch selector

 master

User selector

alexkeizer

Datepicker

All time

Commit History

Commits on Jan 10, 2025

• feat: BitVec.{toFin, toInt, msb}_umod (#6404)

  Show description for 918924c
  

  alexkeizer

  and

  kim-em

  authored
  918924c

  Copy full SHA for 918924c

• feat: BitVec.{toInt, toFin, msb}_udiv (#6402)

  Show description for d2c4471
  

  alexkeizer

  and

  kim-em

  authored
  d2c4471

  Copy full SHA for d2c4471

Commits on Dec 9, 2024

• doc: clarify difference between Expr.hasLooseBVars and Expr.hasLooseBVar (#6344)

  Show description for ff3d12c
  

  alexkeizer

  and

  nomeata

  authored
  ff3d12c

  Copy full SHA for ff3d12c

Commits on Dec 5, 2024

• feat: upstream ToLevel from mathlib (#6285)

  Show description for 1400b95
  

  3 peopleauthored
  1400b95

  Copy full SHA for 1400b95

Commits on Nov 8, 2024

• fix: ensure instantiateMVarsProfiling adds a trace node (#5501)

  Show description for fc0529b
  alexkeizer

  authored
  fc0529b

  Copy full SHA for fc0529b

Commits on Oct 30, 2024

• feat: prove that intMin is indeed the smallest signed bitvector (#5778)

  alexkeizer

  authored
  b5bbc57

  Copy full SHA for b5bbc57

Commits on Oct 15, 2024

• feat: bv_decide inequality regression tests (#5714)

  Show description for 94dd1d6
  

  alexkeizer

  and

  hargoniX

  authored
  94dd1d6

  Copy full SHA for 94dd1d6

Commits on Sep 26, 2024

• chore: remove mention of Lean.withSeconds (#5481)

  Show description for 91a0334
  alexkeizer

  authored
  91a0334

  Copy full SHA for 91a0334

Commits on Sep 20, 2024

• feat: instance for Inhabited (TacticM α) (#5401)

  Show description for d8e0fa4
  alexkeizer

  authored
  d8e0fa4

  Copy full SHA for d8e0fa4

Commits on Sep 18, 2024

• feat: add bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (#5375)

  Show description for 4641ed8
  alexkeizer

  authored
  4641ed8

  Copy full SHA for 4641ed8

Commits on Sep 4, 2024

• refactor: make extractLsb' the primitive bv_decide understands, rather than extractLsb (#5211)

  Show description for fa8439a
  alexkeizer

  authored
  fa8439a

  Copy full SHA for fa8439a

Commits on Aug 14, 2024

• feat: express BitVec.extractLsb' in terms of extractLsb (#5007)

  Show description for bff30fe
  

  alexkeizer

  and

  tobiasgrosser

  authored
  bff30fe

  Copy full SHA for bff30fe

Commits on May 29, 2024

• feat: upstream BitVec.toFin_ofNat and BitVec.toFin_neg (#4298)

  Show description for 9133470
  alexkeizer

  authored
  9133470

  Copy full SHA for 9133470

Commits on May 23, 2024

• feat: bitblasting theorems for signed comparisons (#4201)

  Show description for 4fa3b3c
  

  alexkeizer

  and

  kim-em

  authored
  4fa3b3c

  Copy full SHA for 4fa3b3c

Commits on May 22, 2024

• feat: characterize BitVec.toInt in terms of BitVec.msb (#4200)

  Show description for 23a202b
  

  alexkeizer

  and

  kim-em

  authored
  23a202b

  Copy full SHA for 23a202b

Commits on May 20, 2024

• feat: Nat.shiftLeft_shiftRight (#4199)

  Show description for 42215cc
  alexkeizer

  authored
  42215cc

  Copy full SHA for 42215cc

Commits on May 16, 2024

• feat: bitblasting theorems about unsigned bitvector inequalities (#4178)

  Show description for 2a966b4
  alexkeizer

  authored
  2a966b4

  Copy full SHA for 2a966b4

Commits on Mar 5, 2024

• feat: add lemmas about BitVec.concat and bitwise ops (#3487)

  Show description for 46bf4b6
  alexkeizer

  authored
  46bf4b6

  Copy full SHA for 46bf4b6

Commits on Feb 23, 2024

• feat: add BitVec.toNat_concat (#3471)

  Show description for b9b4d8f
  alexkeizer

  authored
  b9b4d8f

  Copy full SHA for b9b4d8f

• feat: add BitVec.getLsb_concat (#3457)

  Show description for 8bf6475
  

  alexkeizer

  and

  kim-em

  authored
  8bf6475

  Copy full SHA for 8bf6475

Commits on Feb 22, 2024

• refactor: make BitVec.carry take bitvector arguments (#3461)

  Show description for 815200e
  alexkeizer

  authored
  815200e

  Copy full SHA for 815200e

• feat: show basic properties of BitVec multiplication (#3445)

  Show description for 997ae40
  

  alexkeizer

  authored and

  leodemoura

  committed
  997ae40

  Copy full SHA for 997ae40