Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Jan 18, 2025

• fix: make #check_failure's output be info (#6685)

  Show description for 98e3d6f
  Seasawher

  authored
  98e3d6f

  Copy full SHA for 98e3d6f

• fix: grind parameter issues and configuration (#6686)

  Show description for d4070d4
  leodemoura

  authored
  d4070d4

  Copy full SHA for d4070d4

Commits on Jan 17, 2025

• feat: extensionality theorems in grind (#6682)

  Show description for 4d4c094
  leodemoura

  authored
  4d4c094

  Copy full SHA for 4d4c094

• chore: update stage0

  Show description for 9b629cc
  leodemoura

  committed
  9b629cc

  Copy full SHA for 9b629cc

• refactor: move ext environment extension to Lean.Meta.Tactic

  leodemoura

  committed
  f374ef1

  Copy full SHA for f374ef1

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  e3fd954

  Copy full SHA for e3fd954

• feat: add lcAny constant to Prelude (#6665)

  Show description for b7815b5
  zwarich

  authored
  b7815b5

  Copy full SHA for b7815b5

• fix: don't filter out local instances in LCNF toMono pass (#6664)

  Show description for 7f0ae22
  zwarich

  authored
  7f0ae22

  Copy full SHA for 7f0ae22

• feat: add simp-like parameters to grind (#6675)

  Show description for 35a4da2
  leodemoura

  authored
  35a4da2

  Copy full SHA for 35a4da2

Commits on Jan 16, 2025

• chore: remove unneeded instance (#6671)

  Show description for 60142c9
  hargoniX

  authored
  60142c9

  Copy full SHA for 60142c9

• fix: add workaround for MessageData limitations (#6669)

  Show description for 17c0187
  leodemoura

  authored
  17c0187

  Copy full SHA for 17c0187

• feat: equality resolution for grind (#6663)

  Show description for e42f7d9
  leodemoura

  authored
  e42f7d9

  Copy full SHA for e42f7d9

• feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib, shiftLeft_and_distrib, testBit_mul_two_pow, bitwise_mul_two_pow, shiftLeft_bitwise_distrib] (#6630)

  Show description for 906aa1b
  

  luisacicolini

  and

  alexkeizer

  authored
  906aa1b

  Copy full SHA for 906aa1b

• feat: align List.replicate/Array.mkArray/Vector.mkVector lemmas (#6667)

  Show description for f015271
  kim-em

  authored
  f015271

  Copy full SHA for f015271

• feat: Vector.getElem_flatMap (#6661)

  Show description for f4c9934
  kim-em

  authored
  f4c9934

  Copy full SHA for f4c9934

• feat: align List/Array/Vector.flatMap (#6660)

  Show description for 80ddbf4
  kim-em

  authored
  80ddbf4

  Copy full SHA for 80ddbf4

• feat: canonicalizer diagnostics (#6662)

  Show description for 3a6c5cf
  leodemoura

  authored
  3a6c5cf

  Copy full SHA for 3a6c5cf

• fix: grind term preprocessor (#6659)

  Show description for af4a7d7
  

  leodemoura

  and

  kim-em

  authored
  af4a7d7

  Copy full SHA for af4a7d7

• feat: improve case-split heuristic used in grind (#6658)

  Show description for 6259b47
  leodemoura

  authored
  6259b47

  Copy full SHA for 6259b47

Commits on Jan 15, 2025

• refactor: lake: use StateRefT for BuildStore (#6290)

  Show description for 0050e93
  tydeu

  authored
  0050e93

  Copy full SHA for 0050e93

• feat: improve grind search procedure (#6657)

  Show description for 64cf5e5
  leodemoura

  authored
  64cf5e5

  Copy full SHA for 64cf5e5

• feat: more grind tests (#6650)

  Show description for 127b3f9
  kim-em

  authored
  127b3f9

  Copy full SHA for 127b3f9

• feat: improvegrind diagnostic information (#6656)

  Show description for 65175dc
  leodemoura

  authored
  65175dc

  Copy full SHA for 65175dc

• feat: better support for partial applications in the E-matching procedure (#6654)

  Show description for 54f06cc
  leodemoura

  authored
  54f06cc

  Copy full SHA for 54f06cc

• fix: improve E-matching pattern selection heuristics (#6653)

  Show description for b3f8fef
  leodemoura

  authored
  b3f8fef

  Copy full SHA for b3f8fef

• feat: verify insertMany method for adding lists to HashMaps (#6211)

  Show description for 6665837
  

  monsterkrampe

  and

  jt0202

  authored
  6665837

  Copy full SHA for 6665837

• feat: tag lemmas

  

  hargoniX

  authored and

  Kha

  committed
  c7fd873

  Copy full SHA for c7fd873

• chore: update stage0

  

  hargoniX

  authored and

  Kha

  committed
  a10ce94

  Copy full SHA for a10ce94

• feat: add the int_toBitVec simpset

  

  hargoniX

  authored and

  Kha

  committed
  838ad28

  Copy full SHA for 838ad28

• perf: improve bv_decide preprocessing based on Bitwuzla optimisations (#6641)

  Show description for a1ef26b
  hargoniX

  authored
  a1ef26b

  Copy full SHA for a1ef26b

• fix: grind canonicalizer state management (#6649)

  Show description for a955708
  leodemoura

  authored
  a955708

  Copy full SHA for a955708

• fix: indicate dependency on pkgconf in ubuntu docs (#6646)

  Show description for 0f7f80a
  kim-em

  authored
  0f7f80a

  Copy full SHA for 0f7f80a

• feat: literals, lower and upper bounds in the offset constraint module within grind (#6648)

  Show description for 8d69909
  leodemoura

  authored
  8d69909

  Copy full SHA for 8d69909

• chore: fib_correct monadic reasoning example as a test (#6647)

  Show description for f95d810
  kim-em

  authored
  f95d810

  Copy full SHA for f95d810

• feat: align List/Array/Vector flatten lemmas (#6640)

  Show description for 5d6bf75
  kim-em

  authored
  5d6bf75

  Copy full SHA for 5d6bf75

Pagination

Previous

Next