All pull requests

Pull requests

• feat: new deriving framework

  toolchain-available
  #15320·Rob23oba opened Sep 25, 2026Contributor·

  ·

• feat: add Expr.hasAnyMVar analogous to Expr.hasAnyFVar

  changelog-languagetoolchain-available
  #15319·Rob23oba opened Sep 25, 2026Contributor·

  ·

• feat: add a DiscrTree.getEntriesWithKeys function

  changelog-languagetoolchain-available
  #15318·Rob23oba opened Sep 25, 2026Contributor·

  ·

• feat: add Bool.dand and Ordering.dthen along with more lemmas

  changelog-librarytoolchain-available
  #15317·Rob23oba opened Sep 25, 2026Contributor·

  ·

• fix: remove duplicate BEq (Option a) instance

  #15316·Rob23oba opened Sep 25, 2026Contributor·

  ·

• fix: Array.compareLex to be specialized correctly

  changelog-librarytoolchain-available
  #15315·Rob23oba opened Sep 25, 2026Contributor·

  ·
  2

• fix: inconsistency in functions about private names

  changelog-notoolchain-available
  #15309·Rob23oba opened Sep 24, 2026Contributor·

  ·
  1

  2

• chore: missing order instances for List, Array and Vector

  changelog-librarydownstreamtoolchain-available
  #15304·TwoFX opened Sep 24, 2026Member·

  ·
  1

• feat: grind norm automation for the lattice theory

  toolchain-available
  #15299·sgraf812 opened Sep 24, 2026Contributor·

  ·

• feat: add lemmas for disjointness of unions

  toolchain-available
  #15294·joehattori opened Sep 23, 2026·

  ·
  1

• perf: memoize the search path root of each package in findOLean

  toolchain-available
  #15291·casavaca opened Sep 23, 2026Contributor·

  ·
  1

• perf: inline more specialize less

  toolchain-available
  #15285·hargoniX opened Sep 23, 2026Member·

  ·
  2

• doc: correct docstring for Dyadic.pow

  toolchain-available
  #15283·LLaurance opened Sep 23, 2026·

  ·

• feat: record option dependencies during typeclass synthesis

  changelog-notoolchain-available
  #15278·Kha opened Sep 22, 2026Member·

  ·
  2

• perf: make USize folding more aggressive

  changelog-compilerfsanitize-citoolchain-available
  #15277·hargoniX opened Sep 22, 2026Member·

  ·

• feat: add fast leading and trailing zero counts for machine integers

  changelog-librarytoolchain-available
  #15273·kim-em opened Sep 22, 2026Collaborator·

  ·
  1

• doc: clarify the definition of Nat.lt

  changelog-doctoolchain-available
  #15272·SkanderBog opened Sep 22, 2026·

  ·
  1

  1

• fix: avoid following root symlinks during recursive deletion

  changelog-librarytoolchain-available
  #15271·SkanderBog opened Sep 22, 2026·

  ·
  1

  1

• feat: add show_patterns to grind tactic mode

  changelog-tacticstoolchain-available
  #15270·SkanderBog opened Sep 22, 2026·

  ·
  1

  3

• perf: speed up bitvector leading and trailing zero counting

  changelog-librarytoolchain-available
  #15269·kim-em opened Sep 22, 2026Collaborator·

  ·
  1

• perf: count arbitrary-precision trailing zero bits efficiently

  changelog-librarytoolchain-available
  #15265·kim-em opened Sep 22, 2026Collaborator·

  ·
  1

• feat: mark BitVec.toInt_signExtend as grind_hom

  toolchain-available
  #15262·andres-erbsen opened Sep 22, 2026·

  ·

• feat: add grind_hom annotation to BitVec.toNat_ofInt

  toolchain-available
  #15259·andres-erbsen opened Sep 21, 2026·

  ·

• perf: keep dependent tasks on a warm worker in the task manager

  changelog-compilerdownstreamtoolchain-available
  #15258·Kha opened Sep 21, 2026Member·

  ·
  3

• fix: preserve literal plus signs in HTTP query encoding

  changelog-librarytoolchain-available
  #15254·SkanderBog opened Sep 21, 2026·

  ·
  1

  1