Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 9, 2025

• chore: replace `ByteSubarray` with `ByteSlice` (#1443)

  fgdorais

  authored
  a05c7c7

  Copy full SHA for a05c7c7

• fix: Remove redundant attribute declaration (#1452)

  linesthatinterlace

  authored
  c43d86a

  Copy full SHA for c43d86a

Commits on Oct 7, 2025

• fix: Remove `proof_wanted` (#1436)

  Show description for 4702a8b
  

  linesthatinterlace

  and

  fgdorais

  authored
  4702a8b

  Copy full SHA for 4702a8b

• refactor: Nat.sqrt: avoid reducing wfrec (#1447)

  nomeata

  authored
  00cdd05

  Copy full SHA for 00cdd05

• refactor: Fin.dfoldlM: avoid reducing wfrec (#1448)

  nomeata

  authored
  b1fc386

  Copy full SHA for b1fc386

• refactor: WF.recC: avoid reducing wfrec (#1449)

  nomeata

  authored
  e2e7d88

  Copy full SHA for e2e7d88

Commits on Oct 6, 2025

• chore: forward port of lean4#10627 (#1433)

  fgdorais

  authored
  5de3b92

  Copy full SHA for 5de3b92

Commits on Sep 29, 2025

• feat: add `Fin.findSome?_eq_some_iff` and `Fin.find?_eq_some_iff` (#1431)

  Show description for 6f7d05f
  

  linesthatinterlace

  and

  fgdorais

  authored
  6f7d05f

  Copy full SHA for 6f7d05f

• docs: update Mathlib adaptation process (#1428)

  fgdorais

  authored
  9e2a0dd

  Copy full SHA for 9e2a0dd

Commits on Sep 23, 2025

• refactor: define List.IsChain, deprecate Chain and Chain' (#1421)

  Show description for 903b509
  

  linesthatinterlace

  and

  fgdorais

  authored
  903b509

  Copy full SHA for 903b509

Commits on Sep 20, 2025

• feat: support realized names in `open private` (#1417)

  digama0

  authored
  e91bd23

  Copy full SHA for e91bd23

Commits on Sep 15, 2025

• chore: bump toolchain to v4.24.0-rc1 (#1415)

  Show description for 3881bc9
  

  18 peopleauthored
  3881bc9

  Copy full SHA for 3881bc9

Commits on Sep 14, 2025

• chore: bump toolchain to v4.23.0 (#1413)

  kim-em

  authored
  d117e2c

  Copy full SHA for d117e2c

Commits on Sep 12, 2025

• feat: add some grind annotations / proofs in Data/List/Lemmas (#1411)

  kim-em

  authored
  a9a0cb7

  Copy full SHA for a9a0cb7

Commits on Sep 8, 2025

• feat: add `Char.all`, `Char.any` and decidability instances (#1344)

  Show description for cd9ede0
  

  3 peopleauthored
  cd9ede0

  Copy full SHA for cd9ede0

• feat: lemmas about `throw` and `tryCatch` for `ReaderT` and `StateT` (#1406)

  eric-wieser

  authored
  3dedd9b

  Copy full SHA for 3dedd9b

• feat: more support for `AlternativeMonad` (#1405)

  eric-wieser

  authored
  15d03b2

  Copy full SHA for 15d03b2

• feat: add iterator transformer for KMP matcher (#1398)

  fgdorais

  authored
  8236ad6

  Copy full SHA for 8236ad6

Commits on Sep 1, 2025

• feat: add `@[simp]` lemma `WellFounded.val_wrap` (#1308)

  Show description for a67fc66
  

  plp127

  and

  kim-em

  authored
  a67fc66

  Copy full SHA for a67fc66

Commits on Aug 30, 2025

• feat: better Newton starting point in `Nat.sqrt` (#1395)

  kim-em

  authored
  eebfdee

  Copy full SHA for eebfdee

Commits on Aug 26, 2025

• feat: add case insensitive comparison for strings (ASCII only) (#1283)

  Show description for 76408f0
  

  ammkrn

  and

  fgdorais

  authored
  76408f0

  Copy full SHA for 76408f0

Commits on Aug 15, 2025

• chore: bump toolchain to v4.23.0-rc2 (#1379)

  kim-em

  authored
  6e89c73

  Copy full SHA for 6e89c73

Commits on Aug 14, 2025

• chore: replace a `let` with `have` (#1377)

  ShreckYe

  authored
  4eb3af5

  Copy full SHA for 4eb3af5

• chore: bump toolchain to v4.23.0-rc1 (#1376)

  Show description for dc46fbd
  

  18 peopleauthored
  dc46fbd

  Copy full SHA for dc46fbd

Commits on Aug 11, 2025

• chore: propose deprecation of List.fillNones (#1369)

  kim-em

  authored
  1340120

  Copy full SHA for 1340120

Commits on Aug 8, 2025

• feat: minor cleanup around Rat (#1365)

  kim-em

  authored
  f896bbb

  Copy full SHA for f896bbb

• feat: add Hashable instance to Rat (#1349)

  Show description for aaf3447
  

  Seasawher

  and

  fgdorais

  authored
  aaf3447

  Copy full SHA for aaf3447

Commits on Aug 7, 2025

• Revert "chore: propose deprecation List.fillNones"

  Show description for c4277d9
  kim-em

  committed
  c4277d9

  Copy full SHA for c4277d9

• chore: propose deprecation List.fillNones

  kim-em

  committed
  1e51212

  Copy full SHA for 1e51212

Commits on Aug 6, 2025

• feat: add code action to generate `match` cases (#1307)

  Show description for a8aacd1
  

  MoritzBeroRoos

  and

  fgdorais

  authored
  a8aacd1

  Copy full SHA for a8aacd1

Commits on Aug 4, 2025

• doc: fix a typo in README.md (#1358)

  ShreckYe

  authored
  3f34c24

  Copy full SHA for 3f34c24

• chore: deprecate old comparison classes (#1306)

  fgdorais

  authored
  43c277c

  Copy full SHA for 43c277c

Commits on Aug 1, 2025

• fix: use `semiOutParam` in `LawfulMonadState` (#1359)

  JovanGerb

  authored
  6a49e4c

  Copy full SHA for 6a49e4c

Commits on Jul 31, 2025

• chore: remove >6 month deprecations (#1357)

  kim-em

  authored
  bea1ecc

  Copy full SHA for bea1ecc

Commits on Jul 28, 2025

• feat: enable unusedSimpArgs linter (#1351)

  kim-em

  authored
  46f90e2

  Copy full SHA for 46f90e2

Pagination

Previous

Next