Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on May 16, 2025

• fix: lake: `import Lake` w/ precompiled modules on MacOS (#8383)

  Show description for c8290bd
  tydeu

  authored
  c8290bd

  Copy full SHA for c8290bd

• fix: tests that suffer from renaming (#8386)

  hargoniX

  authored
  b7b9589

  Copy full SHA for b7b9589

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  e46daa8

  Copy full SHA for e46daa8

• feat: pretty print `letFun` using `have` syntax (#8372)

  Show description for 3854ba8
  kmill

  authored
  3854ba8

  Copy full SHA for 3854ba8

• feat: revamp aux decl name generation (#8363)

  Show description for 4d58a3d
  Kha

  authored
  4d58a3d

  Copy full SHA for 4d58a3d

• fix: mapError to store message data context (#8375)

  Show description for 6b7a803
  nomeata

  authored
  6b7a803

  Copy full SHA for 6b7a803

• chore: update DTreeMap proofs with more unfolding induction (#8382)

  Show description for 0e96318
  nomeata

  authored
  0e96318

  Copy full SHA for 0e96318

• chore: try refining some benchmark settings (#8377)

  Kha

  authored
  7994e55

  Copy full SHA for 7994e55

• chore: update stage0

  

  Lean stage0 autoupdater

  committed
  d24aa91

  Copy full SHA for d24aa91

• feat: more parameters in `.fun_cases` theorem (#8359)

  Show description for e7b6123
  nomeata

  authored
  e7b6123

  Copy full SHA for e7b6123

• chore: build `leanc` with Lake under `USE_LAKE` (#8336)

  Show description for af7eb01
  Kha

  authored
  af7eb01

  Copy full SHA for af7eb01

• chore: variants of `dite_eq_left_iff` (#8357)

  Show description for ca9b3eb
  TwoFX

  authored
  ca9b3eb

  Copy full SHA for ca9b3eb

• chore: adopt Option.getD (#8374)

  zwarich

  authored
  a817067

  Copy full SHA for a817067

• fix: revert #8023 now that it is redundant (#8371)

  Show description for fcb6bce
  zwarich

  authored
  fcb6bce

  Copy full SHA for fcb6bce

• chore: cleanup previously failing grind test (#8370)

  Show description for 73509d0
  kim-em

  authored
  73509d0

  Copy full SHA for 73509d0

Commits on May 15, 2025

• fix: `instantiateTheorem` in `grind` (#8369)

  Show description for 6448547
  leodemoura

  authored
  6448547

  Copy full SHA for 6448547

• feat: add an LCNF pass to convert structure projections to cases expressions (#8367)

  Show description for 632b688
  zwarich

  authored
  632b688

  Copy full SHA for 632b688

• fix: give Ordering.then the `expose` attribute (#8366)

  Show description for c5335b6
  zwarich

  authored
  c5335b6

  Copy full SHA for c5335b6

• fix: use `withReducibleAndIntances` to match ground patterns (#8365)

  Show description for a594f65
  leodemoura

  authored
  a594f65

  Copy full SHA for a594f65

• feat: basic support for eta reduction in `grind` (#7977)

  Show description for 7a6bca5
  

  leodemoura

  and

  kim-em

  authored
  7a6bca5

  Copy full SHA for 7a6bca5

• fix: cases tactic to handle non-atomic eliminator well (#8361)

  Show description for e5393cf
  nomeata

  authored
  e5393cf

  Copy full SHA for e5393cf

• fix: FunInd: strip MData when creating the unfolding theorem (#8354)

  Show description for 3481f43
  nomeata

  authored
  3481f43

  Copy full SHA for 3481f43

• fix: FunInd: clean up packed arguments more throughly (#8356)

  Show description for 528fe0b
  nomeata

  authored
  528fe0b

  Copy full SHA for 528fe0b

• feat: do not export def bodies by default (#8221)

  Show description for 01dbbee
  

  Kha

  and

  TwoFX

  authored
  01dbbee

  Copy full SHA for 01dbbee

• chore: tame some slow benchmarks (#8352)

  Show description for 9486421
  Kha

  authored
  9486421

  Copy full SHA for 9486421

• fix: deduplicate elaboration of constant argument to `rw` (#8232)

  Show description for d69a8ef
  JovanGerb

  authored
  d69a8ef

  Copy full SHA for d69a8ef

• feat: preparation for semirings and noncommutative rings in grind (#8343)

  Show description for 8154aaa
  kim-em

  authored
  8154aaa

  Copy full SHA for 8154aaa

• chore: fix `Inv.inv` notation (#8351)

  kim-em

  authored
  abc85c2

  Copy full SHA for abc85c2

• fix: fix typo in inhabited instance for ExtDHashMap (#8349)

  Show description for 4362219
  javra

  authored
  4362219

  Copy full SHA for 4362219

• chore: change chatty test to interactive test (#8348)

  Kha

  authored
  49369f9

  Copy full SHA for 49369f9

• feat: missing lemmas about Int order/multiplication (#8346)

  Show description for 305fba6
  kim-em

  authored
  305fba6

  Copy full SHA for 305fba6

• chore: upstream Inv notation typeclass (#8345)

  kim-em

  authored
  8300121

  Copy full SHA for 8300121

• fix: `etaStruct` and preprocessing issues in `grind` (#8344)

  Show description for 06ef738
  leodemoura

  authored
  06ef738

  Copy full SHA for 06ef738

• chore: initial work on `grind` attributes for `TreeMap` (#8342)

  kim-em

  authored
  37529a5

  Copy full SHA for 37529a5

• fix: `propagateCtor` (#8341)

  Show description for fad3e0e
  leodemoura

  authored
  fad3e0e

  Copy full SHA for fad3e0e

Pagination

Previous

Next