All pull requests

Pull requests

• [#15444] perf: faster interpreter

  adaptationcache-availabletoolchain-available
  #128·downstream-lean4[bot] opened Oct 3, 2026Bot·

  ·
  3

• [#15438] feat: allow reporting positions above #guard_msgs

  adaptationcache-availabletoolchain-available
  #127·downstream-lean4[bot] opened Oct 2, 2026Bot·

  ·
  1

• fix: verso breakage from the SubVerso examples-mechanism removal

  cache-available
  #126·downstream-lean4[bot] opened Oct 2, 2026Bot·

  ·
  1

• [#14421] feat: look for .ilean.mmap files on watchdog load

  adaptationcache-availabletoolchain-available
  #125·downstream-lean4[bot] opened Oct 1, 2026Bot·

  ·
  1

• [#15373] feat: eta-expand partial constructors

  adaptationcache-availabletoolchain-available
  #118·downstream-lean4[bot] opened Sep 28, 2026Bot·

  ·
  1

• [#15374] feat: eta-expand partial recursor apps for structures/K-like types

  adaptationcache-availabletoolchain-available
  #117·downstream-lean4[bot] opened Sep 28, 2026Bot·

  ·
  1

• [#15372] feat: extend unit-like criteria for eta

  adaptationcache-availabletoolchain-available
  #116·downstream-lean4[bot] opened Sep 28, 2026Bot·

  ·
  1

• [#15371] feat: eta-expand recursor major for subsingleton structures

  adaptationcache-availabletoolchain-available
  #115·downstream-lean4[bot] opened Sep 28, 2026Bot·

  ·
  1

• [#15358] [downstream rebase] feat: type class resolution cache stack

  adaptationcache-availabletoolchain-available
  #112·downstream-lean4[bot] opened Sep 27, 2026Bot·

  ·
  10

• [#15351] fix: eta-expand recursor majors before running whnf

  adaptationcache-availabletoolchain-available
  #110·downstream-lean4[bot] opened Sep 27, 2026Bot·

  ·
  3

• [#15339] chore: don't use max precedence for term following private_decl%

  adaptationcache-availabletoolchain-available
  #109·downstream-lean4[bot] opened Sep 26, 2026Bot·

  ·
  1

• subverso maybe?

  cache-available
  #102·Garmelon opened Sep 22, 2026Collaborator·

  ·
  1

• [#15253] feat: better assignment of synthOpaque mvars

  adaptationtoolchain-available
  #100·downstream-lean4[bot] opened Sep 22, 2026Bot·

  ·

• [#14046] chore: rewrite some Fin theorems to use NeZero

  adaptationcache-availabletoolchain-available
  #97·downstream-lean4[bot] opened Sep 22, 2026Bot·

  ·
  2

• [#15258] perf: keep dependent tasks on a warm worker in the task manager

  adaptationcache-availabletoolchain-available
  #96·downstream-lean4[bot] opened Sep 21, 2026Bot·

  ·
  5

• [#15221] feat: better handling of one-field-structure constructors and projections in induction/cases

  adaptationcache-availabletoolchain-available
  #93·downstream-lean4[bot] opened Sep 21, 2026Bot·

  ·
  1

• [#15215] fix: use pi_congr instead of forall_congr, deprecate the latter

  adaptationcache-availabletoolchain-available
  #85·downstream-lean4[bot] opened Sep 18, 2026Bot·

  ·
  3

• [#15210] test: robin's Level.isEquiv

  adaptationcache-availabletoolchain-available
  #83·downstream-lean4[bot] opened Sep 17, 2026Bot·

  ·
  5

• [#15198] test: lean4Lean's Level.isEquiv

  adaptationcache-availabletoolchain-available
  #82·downstream-lean4[bot] opened Sep 17, 2026Bot·

  ·
  3

• [#15138] feat: small stateful linter experiment

  adaptationcache-availabletoolchain-available
  #73·downstream-lean4[bot] opened Sep 12, 2026Bot·

  ·
  1

• [#15109] test toolchain: stricter check for dsimp lemmas

  adaptationcache-availabletoolchain-available
  #68·downstream-lean4[bot] opened Sep 11, 2026Bot·

  ·
  1

• [#15066] feat: virtual one-field structures

  adaptationcache-availabletoolchain-available
  #59·downstream-lean4[bot] opened Sep 8, 2026Bot·

  ·
  1

• [#15027] perf: move ref into the Core.Context cold subobject

  adaptationcache-availabletoolchain-available
  #46·downstream-lean4[bot] opened Sep 4, 2026Bot·

  ·
  1

• [#15002] feat: HTML-like syntax

  adaptationcache-availabletoolchain-available
  #35·downstream-lean4[bot] opened Sep 2, 2026Bot·

  ·
  1

• [#14970] perf: give currRecDepth its own ReaderT layer in CoreM

  adaptationcache-availabletoolchain-available
  #31·downstream-lean4[bot] opened Aug 30, 2026Bot·

  ·
  8