All pull requests

Pull requests

• fix: generate public instance names with private section variables

  toolchain-available
  #15340·emerardd opened Sep 26, 2026Contributor·

  ·
  1

• chore: don't use max precedence for term following private_decl%

  changelog-languagedownstreamtoolchain-available
  #15339·thorimur opened Sep 26, 2026Contributor·

  ·
  3

• fix: no more UB with RC access

  fsanitize-citoolchain-available
  #15337·hargoniX opened Sep 25, 2026Member·

  ·
  6

• fix: make lets in function positions evaluate lazily

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

  ·
  6

• perf: beta-reduce lambdas passed to macro_inline definitions

  toolchain-available
  #15332·datokrat opened Sep 25, 2026Contributor·

  ·
  2

• fix: preserve instance binder used in later lambda binder

  toolchain-available
  #15330·emerardd opened Sep 25, 2026Contributor·

  ·
  1

• feat: missing order instances for ByteArray

  changelog-librarytoolchain-available
  #15329·TwoFX opened Sep 25, 2026Member·

  ·

• feat: reverse iterators for Array and Vector

  toolchain-available
  #15327·Bubbler-4 opened Sep 25, 2026·

  ·

• test: keep Init out of the lake check test projects

  toolchain-available
  #15326·Kha opened Sep 25, 2026Member·

  ·

• feat: add safe withIsExclusive wrapper around isExclusiveUnsafe

  changelog-librarytoolchain-available
  #15323·nomeata opened Sep 25, 2026Collaborator·

  ·
  1

  12

• fix: introduce __-prefixed binders as implementation details in Sym.intros

  toolchain-available
  #15322·sgraf812 opened Sep 25, 2026Contributor·

  ·

• perf: keep borrow annotations when inlining partial applications

  toolchain-available
  #15321·datokrat opened Sep 25, 2026Contributor·

  ·
  2

• feat: new deriving framework

  changelog-languagetoolchain-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

  changelog-librarytoolchain-available
  #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 lemmas for the lattice theory

  changelog-librarytoolchain-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·

  ·